Class 1: Foundations of Proof Assistants

Our first class will be a lecture about the foundations of proof assistants. It will be based loosely on Chapters 1 and 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. Reading this is optional, but recommended.

QED at Large is a survey paper about engineering formally verified proofs of program correctness. Chapter 1 is the introduction. 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.

You can find a reading guide and some discussion questions below. The slides for the class are here.

I actually wrote a whole reading guide for this paper a couple of years ago, so please check it out if it helps you! Please also see the errata.

I'll cover this in class, but in Chapter 1, I think the coolest thing to note is the (very briefly mentioned) de Bruijn criterion, which allows for this beautiful separation of concerns between the proof automation we'll build in this class and the core proof checker. Basically, it's the reason you can slap something fancy like a neural network on top of your proof assistant if you'd like, and still know that you'll never break the actual proof assistant.

Chapter 4 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. We'll get into this more the next two classes!

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. We'll see more of this soon, and I'll talk about it in class.
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.

Since the reading is optional, there is no need to post in the class forum thread, but feel free to do so if interested. Regardless, thinking about any one of these questions may help you better internalize the reading or lecture.

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.