This is a very interesting paper, available here. Its

main thesis is that formal program verification is inherently flawed,

and can never work. The argument in favor of formal verification goes

something like this: computer programming is like

mathematics. Mathematicians use proofs to show correctness. Proofs

start from point A and by a series of correct steps reach point B. If

A is correct and the steps are correct, B must be correct. We can

apply the same process to programs and show that they are correct as

well.

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?