Class 5: Languages for Automation

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.

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.

Section 5.1 talks about different styles of automation---these are all really important, and you should try to get a high-level idea of how each of them works. But it's normal and fine to be confused about the details; feel free to ask questions.

I would not worry too much about fully understanding the examples unless you'd really like to; my hope is that you will get a lot more out of playing with the automation in class on Thursday.

Section 5.2 talks about some cool custom automation in practice. I would just let this be an inspiration for some of what we'll read in later weeks, again without worrying too much about details unless you find them super interesting.

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 once again that you are designing a new proof assistant, and that you have already chosen its foundations. You are now weighing whether to build a language for automation on top of the foundations and, if so, what the language should be like, and what kind of automation it should support. What do you consider in your design, and why?
2. Agda makes a deliberate choice not to include a separate language for automation, sticking to just proofs by reflection. What do you think of this choice, and why?
3. Section 5.1 details a number of example languages for proof automation, like OCaml, Ltac, and Isabelle/Isar. Which do you think you'd find most natural to use, and why?
4. Suppose that you are tasked with building a new language for proof automation, with an emphasis on readability and proof understanding. How do you design your language?
5. What properties of a language for proof automation do you think are most important? And what properties do you think are least important?
6. What do you think the tradeoffs are of using general-purpose, powerful automation like a hammer, versus using lower-level automation like application and rewriting?
7. Write a paragraph responding to someone else's comment in the discussion forum.
8. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.

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.