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