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?
Muli Ben-Yehuda's journal 
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 |