I know it is possible. But I wonder what stops us from doing it for most programs we write from day to day. And, if proving correctness is indeed important (I believe so), can we do something / what is the next thing to do to enable us proving correctness in our daily job.
What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is almost never worth it.
We hope that this cost can be lowered in the future.
The commonplace languages in use are difficult to reason about. It would take a serious paradigm shift for most companies to stop what they're doing and develop a tool chain for wholesale program verification. Additionally, it takes a special breed of programmer to be able and willing to write code in such a way that enables verification, then actually take the time to verify it. Functional programming is a jump for most main stream engineers, it is an altogether different matter to recruit or develop a team of engineers familiar with dependent type theory and formal verification.
The industry tends to lag behind academia by at least a couple decades. In the 90's, lots of research was being devoted to functional programming and the various applications of type systems. Now we see various companies starting to use languages like Haskell and ocaml. Nowadays, it seems like dependent types and program verification are popular in academia, so maybe we'll see some of that by 2030.
For an example of what mafibre is talking about: even proving that a BubbleSort implementation is correct is quite tricky.
First of all, you need to correctly define the specification. Saying "the returned list is sorted" isn't enough because that would also accept lists that have nothing to do with the input, like [1,2,3,4,5]. Also saying that the list only contains elements from the input is also not enough because that would accept a returned list with duplicated or missing elements. To really make a specification that models what you want you need to say that the returned list is a sorted permutation of the input list.
Then, once you manage to get a formal specification that is actually what you want prout invariantving it is also hard. In the bubble sort case you need to figure you need to write down the proofs in detail, down to the point when you use the fact that comparison is a transitive relation.
