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:

- 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.
- 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.
- The notion of a
**proof object**, which is the core certificate that a proof assistant checks for correctness in the end.
- 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.