## Reading

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**.