Muli Ben-Yehuda (mulix) wrote,
Muli Ben-Yehuda
mulix

Thoughts on Social Processes and Proofs of Theorems and Programs, by De Millo et al.

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?

Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 6 comments