The way I see formal correctness proofs is that they'll be useful, but not a panacea.
If I have a method that takes a List as a parameter, and returns an Integer, then congratulations - I have just written a formal proof that it is possible to derive an Integer from a List.
However, the business need wasn't to derive an Integer from a List - it was something far more specific.
So that's why people like the idea of dependent types, in that you can make the type system (mostly) Turing complete, and actually make the types reflect the specification of the problem.
And then if you write an implementation of that specification, congratulations, you have proved that that implementation is correct.
Which is pretty cool, except that it overlooks the fact that a very large percentage of our bugs are not in our implementation, but in our agreed-upon specification. Almost every bug I encounter (that sneaks its way to QA or production and is reported as a bug) is due to the fact that I validly implemented a specification one way, when the business need actually wanted a slightly different interpretation of the specification, but just wasn't specific enough when they described it.
Anyway, formal correctness proofs won't handle that. Really all it means is that the hard part of programming - making sure we're actually developing the correct thing - will be offloaded from implementation to specification. That means that implementation will be more of a code monkey role, while the real art of programming - interpreting and anticipating needs, a role that programmers are vastly under appreciated for - will need to be accomplished by someone that is sort of like a product owner, but far more technical and exacting than is the norm now. I'd imagine many senior level programmers would move into that role - translating business needs into formal specification, and then leaving junior programmers to monkey with the proof itself.
I don't see formal proofs replacing acceptance tests. I see them helping you build leak-proof abstractions upon which you assemble the domain where your functionality is implemented. The line between those two positions is blurry and, despite the sound of it, your need to be comprehensive with a formal proof also varies due to possibility and value.
All of these things are just tools after all—you use them to produce value. I think you've described one potential future with this technology, but it, I feel, is very narrow.
One thing that does seem to be playing out is that for many interesting programs the establishment of the theorem is sufficiently challenging that the proof need not be relegated to "junior programmers" but instead automated entirely. Of course, that said, typically a primary tool in the search for a well-specific theorem is a long series of failed attempts to prove its poorly-specified predecessors.
If I have a method that takes a List as a parameter, and returns an Integer, then congratulations - I have just written a formal proof that it is possible to derive an Integer from a List.
However, the business need wasn't to derive an Integer from a List - it was something far more specific.
So that's why people like the idea of dependent types, in that you can make the type system (mostly) Turing complete, and actually make the types reflect the specification of the problem.
And then if you write an implementation of that specification, congratulations, you have proved that that implementation is correct.
Which is pretty cool, except that it overlooks the fact that a very large percentage of our bugs are not in our implementation, but in our agreed-upon specification. Almost every bug I encounter (that sneaks its way to QA or production and is reported as a bug) is due to the fact that I validly implemented a specification one way, when the business need actually wanted a slightly different interpretation of the specification, but just wasn't specific enough when they described it.
Anyway, formal correctness proofs won't handle that. Really all it means is that the hard part of programming - making sure we're actually developing the correct thing - will be offloaded from implementation to specification. That means that implementation will be more of a code monkey role, while the real art of programming - interpreting and anticipating needs, a role that programmers are vastly under appreciated for - will need to be accomplished by someone that is sort of like a product owner, but far more technical and exacting than is the norm now. I'd imagine many senior level programmers would move into that role - translating business needs into formal specification, and then leaving junior programmers to monkey with the proof itself.