Class 11: Custom Tactics

For this class, we will read Planning for Change in a Formal Verification of the Raft Consensus Protocol [PDF] [DOI] by Doug Woos, James Wilcox, Steve Anton, Zach Tatlock, Michael Ernst, and Thomas Anderson.

I really love this paper because it gets at a problem I didn't find immediately obvious when I was first learning about proof assistants: Good proof automation isn't just about developing proofs to begin with. It's also about maintaining proofs as the thing we are proving changes over time. And when we are proving properties about programs, well, programs change all the time. So proof maintenance is a really important problem!

The approach taken in this paper is to try to design proofs that are less likely to break over time from the very start---much like software engineers use good design principles to make unverified programs less likely to break over time.

Some of the design principles in this paper mirror traditional software engineering design principles. But the ones around robust custom proof automation are totally new! And corresponding custom automation following these design principles is now available inside of a public library, as we'll see on Thursday.

You can find a reading guide and the discussion questions below. The public version of the slides for this class are 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.

There are really two different things going on here at the same time. The first is the discussion of the formally verified Raft consensus protocol itself---a massive and impressive undertaking. The second is the collection of proof engineering methodologies to make proofs resilient to change that the proof engineers developed in the process of verifying Raft.

To some degree, these two things are inseparable. But for the purposes of this class, it is okay not to understand that much about how the Raft consensus protocol works, or about distributed systems at all. Accordingly, you may find Chapters 4 through 7 particularly relevant to this class.

While the emphasis is on design rather than automation, as with last week's reading, Chapters 5 through 7 yet again drive home the point that these are to some degree inseparable inside of a proof assistant. Focusing on the interplay between design and automation may prove especially fruitful.

If you're super interested in custom tactics in general, and just want to learn more, I strongly recommend reading Certified Programming with Dependent Types by Adam Chlipala.

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. How general do you think the design principles described in this paper are? Do you think they would prove useful for different kinds of proof developments?
2. If you have experience writing proofs inside of a proof assistant---or just based on what you've read about proof assistants so far---are there any other design principles you would employ to make proofs less likely to break over time? How would those design principles interact with automation?
3. Can you think of any ways that automation could help proof engineers employ any of these design principles? If so, what are some ideas you have? They can be speculative.
4. Section 7.1 briefly describes alternative styles of proof automation with tactics in Coq, before settling on the approach the authors take. What do you imagine the tradeoffs are for employing these different styles?
5. Write a paragraph responding to someone else's comment in the discussion forum.
6. 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.