Class 3: Foundations of Proof Assistants

For the third class, we will read Chapter 4 of QED at Large: A Survey of Engineering of Formally Verified Software [PDF] [DOI] by Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock.

Chapter 4 is about the foundations and history of proof assistants---from philosophy to type theory to design. It was mostly written by Karl Palsmkog, who did a fantastic job; I just added a few bits and pieces to that chapter. I hope it will give you some idea of how proof assistants came to be, and what they really are.

This is the second week of background knowledge, which is important for reading later papers. There will be just one more week of background knowledge after this, and then we'll get to the fun stuff.

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

Please note that as POPL is over, this is due the morning before class, so that we can discuss it in person. Also, Thursday will be our first artifact discussion; please install the artifact before Thursday's class.

I again recommend checking out the reading guide for this paper that I wrote a couple of years ago, if it helps you. Please also see the errata.

This chapter at many points goes into a lot of detail about particular logical systems. I think it's okay not to get too bogged down by those details. The core takeaway there is just that the foundations of these tools go back really far, like before computers were even really a thing. Heck, Alan Turing wrote the first proof of program correctness!

It's also good to know, at a high level, that there are a lot of different logical systems that can make up the foundations of proof assistants.

Four things are worth extra attention:

1. The Curry-Howard correspondence, which relates logical systems and type systems, and so also programs and proofs---it's the reason we can write programs and proofs in the same language inside of a proof assistant, if we'd like.
2. Once again, the de Bruijn criterion, which gives us separation of concern between the foundations of our logic and the automation we build on top of it.
3. The notion of a proof object, which is the core certificate that a proof assistant checks for correctness in the end.
4. The notion of a Trusted Computing Base or TCB---the core part of a verified system that is trusted, which people like to try to minimize.

I also really like the discussion of equality, which is one of the hardest problems in type theory; we'll doubtlessly see it pop up in some of the papers we read.

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. Imagine that you are designing a new proof assistant, from the foundations up. What do you consider in your design of the foundations, and why?
2. Alan Turing wrote the first proof of program correctness, and yet Hoare and Floyd are largely credited for the earliest verification work. Why do you think this is?
3. The de Bruijn criterion states that proof assistants should produce proof objects that are checkable by a small kernel that implements the logical system---ideally a kernel that is small enough to be human-readable. What benefits do you think the de Bruijn criterion provides?
4. Section 4.3.1 mentions that some proof assistants produce ephemeral proof objects, which are essentially correct by construction, but never represented and stored in full (though you can reconstruct them after the fact in some proof assistants). This is in contrast with explicit proof objects, which are fully represented---in Coq, for example, proof objects are terms you can modify and type check, just like programs are. Can you think of any tradeoffs between ephemeral and explicit proof objects?
5. Write a paragraph responding to someone else's comment in the discussion forum.
6. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.

We will have this discussion in person, finally! So 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.