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....verification
And Figure 2, "Our analogy", is:
Mathematics Programing
theorem....specification
proof....program
imaginary
formal
demonstration....verification
Note 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?
