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?

Now I have something to read during tomorrow’s taxi to work. Thanks.

Comment by yrk — May 18, 2004 @ 11:04 AM |

Don’t mention it; I hope you enjoy the paper.

I read and am reading a bunch of other itneresting papers and stuff today. I’ll post a list later tonight…

Comment by mulix — May 18, 2004 @ 11:42 AM |

Applying the concept of failure tolerance to math proofs?

My addition to a long list of thanks for letting me know about the paper consists of the following thoughts.

Instead of verifying correctness, successful software developers make their software failure tolerant. On one hand, they cause the software to catastrophically fail rather than sweep bugs under the rug (assert((1+1)==2) is an example of this direction). On the other hand, they add validity checks to subsystem interfaces.

Is it possible to apply the above idea to making mathematical proofs more “error tolerant”? Perhaps by the same way that lawyers argue that their client should prevail in a lawsuit because of A, and even if A was proved to be false, then their client is right because of B, and even if both A and B are disproved, then C ought to win the lawsuit for their client.

Comment by tddpirate — May 18, 2004 @ 1:20 PM |

Re: Applying the concept of failure tolerance to math proofs?

> Instead of verifying correctness, successful software developers make

> their software failure tolerant. On one hand, they cause the software to

> catastrophically fail rather than sweep bugs under the rug

> (assert((1+1)==2) is an example of this direction). On the other hand,

> they add validity checks to subsystem interfaces.

>

> Is it possible to apply the above idea to making mathematical proofs

> more “error tolerant”? Perhaps by the same way that lawyers argue that

> their client should prevail in a lawsuit because of A, and even if A

> was proved to be false, then their client is right because of B, and

> even if both A and B are disproved, then C ought to win the lawsuit for

> their client.

I think there’s a fundamental difference here. In computers, assert (1+1==2) can and *will* fail, because of bit rot, overloading +, gamma rays, whatever. Whereas in a mathematical proof, either 1 + 1 == 2, or not. There’s no “some times”.

Comment by mulix — May 19, 2004 @ 1:13 AM |

The polish effect of Free Software

One way in which Free Software helps advance the state of the art is by doing the equivalent of reformulation of mathematical proofs.

The paper stated that when a mathematician reads a proof, he reformulates it according to his world view. Some theorems and proofs changed their formulations several times during the years, until they converged into extremely simple and elegant forms.

When a company develops a proprietary software package, they cannot make business case for spending the resources to refactor it, to polish it, to make it more (mathematically/aesthetically) elegant. There would not be sufficient increase in income to justify the investment and the loss of opportunity associated with it.

However, in the Free Software world, people can justify investment in polishing an existing software package by the improvement which it adds to their reputation (translation: resume, meaning: better and higher paying job).

The Linux kernel development process illustrates this. Linus intentionally avoids policies, which could freeze intra-kernel module interfaces. So the interfaces change, sometimes drastically, in each major version of Linux. Another example: the process scheduling module has been implemented by different people, using different scheduling algorithms. The scheduling algorithms have undergone a lot of polishing as well. I don’t know if a single scheduling algorithm proved to be superior under all conditions.

Comment by tddpirate — May 18, 2004 @ 1:30 PM |

Re: The polish effect of Free Software

I agree 100%. That’s one of the reasons I think open source is the right way to develop software, just like a mathematical proof that is known only to its author is not worth much to the rest of the world…

Comment by mulix — May 19, 2004 @ 1:14 AM |