Class 27: Looking Back to Look Forward

For the twenty-seventh class and final reading, we will read Social Processes and Proofs of Theorems and Programs [PDF] [DOI] by Richard De Millo, Richard Lipton, and Alan Perlis.

This paper was written by three brilliant researchers in the 1970s, and it basically argues that we just shouldn't do verification at all. So it was quite controversial then---and it's still controversial to this day!

Maybe, then, it seems like a weird call to read this last. But this choice is very deliberate. Because this paper is---ironically---what got me so obsessed that I did my whole thesis in this research area. It really made me angry, honestly, that the authors assumed all of these problems were fundamental, and not solvable. So I got obsessed with solving them. And here I am.

You can find a reading guide and the discussion questions below.

Please note that this is due the morning before class, so that we can discuss it in person.

I honestly really enjoy this paper to this day, as long as I read it as Social Processes and the Next 100 Years of Verification. So I think that's a healthy frame. It's nice to think about what the authors bring up that has been addressed, and what is yet to be addressed, and finally what---in your opinion---is not something that can be addressed at all. This can inspire a lot of future work.

Keeping the historical context in mind is also healthy. The first proof assistants popped up in the early 1970s, and back then, people really hadn't verified anything but toy programs. So you can think about what held true over the last 50 years, and then about what did not hold true.

It's worth noting, also as historical context, that this paper had a long-lasting negative impact on formal verification as a research area. The field was largely abandoned by all but a small group of die-hards, and it was considered very fringe for a long time. But some people like Xavier Leroy just kept churning on and on and on, ushering in the age of "big verification" we finally find ourselves in. God bless people like Xavier Leroy.

Finally, here is an absolutely amazing bonus read: the letters to the editor for this article, complete with an incredible dissent from Leslie Lamport. Basically this is programming languages Twitter before programming languages Twitter was a thing.

Please write a short paragraph as a comment in the class forum thread about any one of the following discussion questions (you need to respond to just one question of your choice to get credit, though you're free to write more if interested):

1. Is there anything in this paper that you strongly agree with? What and why? Do you think the underlying concerns are addressable, and if so, how?
2. Is there anything in this paper that you strongly disagree with? What and why? What would you do to address the corresponding concerns, if anything?
3. What about this paper, if anything, has passed the test of time? And what has not? Why?
4. If you could choose anything in this paper to prove wrong by implementing some new technology for proof engineers, what would you choose, and what would you implement to prove it wrong?
5. This paper stifled the field of program verification for many decades. Do you think there are better ways to critique fields from a position of immense power that do not have this effect?
6. Write a paragraph responding to someone else's comment in the discussion forum.
7. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.

You may want to look at other people's responses before class in order to shape the discussion. And again remember that you need to answer just one question to get credit, though you are free to answer more if interested.