Class 7: Logics & Reflection

For the seventh class, we will read Interactive Proofs in a Higher-Order Concurrent Separation Logic [PDF] [DOI] by Robbert Krebbers, Amin Timany, and Lars Brikedal.

This paper was a suggestion from my friend Tej Chajed. Tej recommended this paper because, in his words, "it's not search-style automation, but what it does do is implement a high-level abstraction (a more sophisticated logic) that happens to look and feel similar to Coq's proof mode. Using only the Iris Proof Mode, and maybe some lightweight extensions, we've been able to carry out pretty big proofs of program correctness. Some of it might be automated further but the [Iris Proof Mode] is really what makes things feasible because each step is at such a high level of abstraction."

In other words, what we have is a cool embedded logic inside of Coq that empowers proof engineers to use powerful automation to reason about programs inside of the embedded logic in a way that feels a lot like writing proofs outside of the embedding.

You can find a reading guide and the discussion questions below.

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.

For this paper, I think the cool things to focus on are the design decisions that make this kind of automation possible, what interacting with it is like, and the problem it solves. It's also really neat to see how it uses computational reflection to implement custom automation for the domain, but exposes an Ltac tactic interface for it.

The introduction, Section 2, and Section 3 are all very useful to read in detail. Section 2 talks about the challenges of reasoning about programs inside of a proof assistant using a few different common methodologies. Section 3 shows what interacting with the automation framework is like, so you can get a sense of the workflow for the implemented automation and the problem it solves.

Section 4 talks about the implementation. This is an interesting read, but it's fine if you get a bit lost about the details. Still, again, I'd pay special attention to the discussion of computational reflection. Hopefully we'll get a chance to dive into this when we look at the artifact on Thursday, and then we can get an even better sense of what's going.

Sections 5 and 6 show the framework in action on an example and a large case study. These are good reads too, but it's very natural to get lost on the details of particular case studies. When we dive into the artifact, I hope these will be easier to follow, too.

Section 7, the evaluation, is short enough that you may as well read the whole thing.

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. Do you agree with the claim that the method is very generic? Why or why not?
2. When reasoning within an embedded logic, would you prefer automation that resembles interacting with your proof assistant normally, or custom automation that looks quite different? Why?
3. What key design decisions do you think most contributed to making this automation framework possible? Do you think there are lesssons one could take away for that for designing other kinds of automation?
4. What do you think the authors gain from implementing custom tactics using reflection? Would you have made the same choice? Do you think anything is lost from this choice? Why or why not?
5. Type classes add a lot of modularity here. In practice, though, type class search can sometimes prove unwieldy for large proof developments with many instances. Do you think this could pose problems in this framework on larger proof developments? If not, why not? And if so, how might you go about designing automation that scales to those larger proof developments?
6. Write a paragraph responding to someone else's comment in the discussion forum.
7. 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.