De Millo's argument is that mathematical theorems are *not*
considered correct because of the mere fact that they have been
"proved". They are considered correct because mathematicians discussed
the proofs with their colleagues, reviewed them, rephrased them in
their own language and applied them elsewhere, and thus came to be
convinced that the proof is indeed correct. It's the conviction that
counts, not the mere technicality of the proof. With formal
verification, such conviction can never happen, since the proof is far
too long and unwieldy to discuss informally, or even thing about and
comprehend. One either believes that the proof is correct, or one
doesn't, on blind faith alone. And blind faith, claims De Millo, is
not sufficient for us to trust a program.

While reading the paper, I kept thinking of what seem to me an obvious solution. Open Source! Rather than looking at a "proof" or a program, let's look at the program itself. The source of a program can be discussed, analyzed, modified and reapplied, in the same way that a good mathematical proof is handled. A program, just like a mathematical proof, is better if it's simple. The similarities are striking. Near the end of the paper, I saw that De Millo apparently shares the opinion, although he never comes out and says so. Figure 1, "the verifiers' original analogy" is:

Mathematics Programing theorem....program proof....verificationAnd Figure 2, "Our analogy", is:

Mathematics Programing theorem....specification proof....program imaginary formal demonstration....verificationNote that the program in De Millo's analogy is its own "mathematical proof".

Points to ponder: ok, so formal verification is inherently flawed, and open source might be the solution. What now?