Muli Ben-Yehuda's journal

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?