Discussion About Proving—Again
Deja Vu All Over Again—Yogi Berra
Rich DeMillo is one of my greatest friends, colleagues, and terrific co-authors. He is currently fighting an illness, and we wish him the best.
Rich was the key guest for Harry Lewis’s class last June. This time it is my turn to be part of the discussion of our paper Social Process and Proofs of Theorems and Programs that starts:
Many people have argued that computer programming should strive to become more like mathematics. Maybe so, but not in the way they seem to think.
Sadly the paper’s third author, Alan Perlis, is unable to ever take part.
The Class
Lewis’s class is based on his book.
The book highlights results that played a key part in the history of CS. Ideas That Created the Future collects forty-six classic papers in computer science that map the evolution of the field. It covers all aspects of computer science: theory and practice, architectures and algorithms, and logic and software systems, with an emphasis on the period of 1936-1980 but also including important early work. Offering papers by thinkers ranging from Aristotle and Leibniz to Alan Turing and Nobert Wiener, the book documents the discoveries and inventions that created today’s digital world. Each paper is accompanied by a brief essay by Harry Lewis, the volume’s editor, offering historical and intellectual context.
Some have asked: How could Rich and Alan and myself be included with such notables? Many hate our paper, but perhaps that is just life. This Tuesday it will be discussed again.
Our Paper
Rich and I were in the late 1970’s quite interested in program correctness. We had three approaches:
The Debate—Starts
The key to the argument is two part:
- The correctness of real systems is not clean. It is very complex, very case based. Terribly complex.
- The proof method of math is not geared to huge complex statements of correctness.
The Debate—Continues
Today papers on proof methods split into two classes:
- Those that refer to us. Usually negatively, but do at least they refer to us.
- Those that ignore us completely.
Here are three examples from countless many papers: They should reference us but do not:
- Philosophical Interests in Program Verification
- Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools
- Correctness: A Very Important Quality Factor In Programming
Open Problems
Should there be some middle ground? Do we deserve to be in Harry’s book?
Honestly, I think you deserve the Turing Award. To me, you are on the same level as Richard M. Karp, who has already been a winner of that award since 1985.
For a book about other people’s work, Lewis’s book is extremely expensive. Is it because the publisher had to pay so much to get the right to reproduce all those great papers? I’m glad I’ve read most of them but it would be nice to read them again after so many years.
Is there a verification issue with example 1?