Retrospective: An Axiomatic Basis for Computer Programming
dl.acm.org
dl.acm.org
The math and algorithms are working, and some very smart (and very pleasant, I might add) people are working around the clock, including from e.g. the French Commission for Nuclear Energy.
However, the learning curve is too high and the developer-experience is very poor at the moment. This is a classic case of gaps between research material and usability.
Fortunately, I see this as where software is headed, especially languages people love to tout as being "unsafe", such as C.
The article is exactly right - tests only test the programmer, not the program. Formal verification is The Way, in my opinion.
In a software project with sufficiently complicated features/requirements, I'd imagine the formal specification is likely as complicated as the program itself. There are ways to make the specification language less error prone, but... that's what the software community has already been doing for decades, by inventing new high level programming languages that are easier to read/write and less prone to error.
IMHO the advances we've seen in high level languages in the past couple decades is in a sense equivalent to formal verification (at least verification of lower level languages like C). Heck, a lot of languages compile down into C as an intermediate form. Although we don't usually think of it that way, I'd say they are as close as "a formal specification language for C" as you can realistically hope for. And as an added bonus, it generates "provably equivalent" C code and thus saves you from writing it explicitly.
That said, there might be value in re-writing code again and proving that the two pieces of code are functionally equivalent. I'm not sure this would be an easy sell from a commercial standpoint though... If systems were important enough that that warrants approaches like this, one can always ask _three_ teams to implement a spec separately, and then take the result of the majority...
I think I'm oversimplifying it, but as I understand they write the entire prover as a proof theorum itself, then use an alternative prover to prove the original theorum, then they write the program and use the proofs to proof itself.
Lots of good academia surrounding that portion of it. Further, assuming I'm reading your implication correctly, languages like Go, Rust or Zig do NOT have formal verification properties to them. They definitely have some neat anti-footgun tools, but they are very far away from formally specified code.
A copy of the original paper from Hoare: