For the fifth class, we will read Chapter 5 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 5 is about proof automation, finally! In particular, recall that the de Bruijn criterion states that these proof assistants produce proof objects that a small kernel can check. Here we learn about how automation can produce those proof objects, without asking the proof engineer to understand all of the low-level details of how the proof assistant works. Thanks to de Bruijn, we get all of this with the guarantee that we do not sacrifice correctness of the proof assistant, which is super powerful.
This is the final week of background knowledge, so next week we'll get to the fun stuff.
You can find a reading guide and the discussion questions below. A public version of the slides I will open this discussion with (with the quotes from student discussions redacted) is available here.
Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.