On Thursday June 17 I went to (on zoom- does that need to be added anymore?)
A Debate on Program Correctness
There was no subtitle but it could have been:
Have the points made in Social Processes and Proofs of Theorems and Programs by DeMillo, Lipton, Perlis, survived the test of time ? (Spoiler Alert: Yes.)
I found out about it from the Lipton-Regan blog here
The debaters were Richard DeMillo and Richard Lipton and the moderator was Harry Lewis (Alan Perlis passed away in 1990). Calling it a debate is not correct since DeMillo and Lipton (and Lewis) all agree. (DeMillo and Lipton even have the same first name!) The DLP paper is in Harry Lewis's collection Ideas that created the future. The event should have been advertised as a discussion. However, it was a good discussion so this is not a complaint.
Here are some things that came out of the discussion.
1) The main topic was the 1979 DeMillo-Lipton-Perlis paper (see here) that gave arguments why Proofs of Program correctness could not work.
An all-to-brief summary of the DLP paper: Some researchers are trying to set up frameworks for doing proofs that programs are correct, analogous to the certainty we get with a proof of a Theorem in Mathematics. But proofs in Mathematics are, in reality, NOT that rigorous. Often details are left out or left to the reader. This is fine for mathematics (more on that later) but unacceptable for programs which need rather precise and rigorous proofs.
How do theorems in mathematics really get verified? By having enough people look at them and make sure they match intuitions, what DLP call A Social Process. (NOTE FROM BILL: Papers that are not important do not get looked at so there may well be errors.)
2) The notion of proving-programs-correct was very seductive; however, the people who were trying to do this had a blind spot about how the analogy of proving-programs-correct and proving-theorem-correct differ. In particular, a program is rather complicated and even stating carefully what you want to prove is difficult. By contrast, for most math statements, what you want to prove is clear. Note also that a program has lots of code (far more now than when DLP was written) and so much can happen that you cannot account for.
3) The DLP paper had a large effect on the field of program verification. Funding for it was reduced and students were discouraged from going into it.
4) When DLP appeared DeMillo and Lipton were pre-tenure. Hence it took lots of courage to publish it. Alan Perlis had tenure and had already won a Turing award. This did give DeMillo and Lipton some cover; however, it still took courage.