Class 15

Today, we will read Proof Repair across Type Equivalences [PDF] [DOI] by Talia Ringer, RanDair Porter, Nate Yazdani, John Leo, and Dan Grossman.

This is my work, so I'm obviously biased. But it's the sort of seminal paper of my thesis work on proof repair, or automatically fixing proofs in response to breaking changes. This is for those cases where you don't manage to design things perfectly to begin with, or when a dependency breaks in an unexpected way.

While proof repair has a while to go before it's a common part of proof development, this was the first time we really showed practical applicability. Shameless plug: I have plenty of ongoing work in this space with my students, so super please let me know if you find any of this particularly interesting and want to work on it!

You can find a reading guide and the discussion questions below. A public copy of the slides for this class can be found 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 don't want to bias folks too much, since this is my seminal thesis paper. But if you are interested in learning more, I do recommend checking out my thesis, which includes a lot more context. My thesis also includes a much prettier explanation of the conditions for correctness of a configuration, and explains what a configuration really is, semantically. So type theory and category theory nerds like me may appreciate that a lot.

If you are more of a video person, the PLDI 2021 talk may help, as may my thesis defense.

In any case, it is totally normal not to understand everything in this paper. This is especially true for Section 4. I think good goals are getting a general sense of how things work, piquing your curiosity for some of the technical details if interested, and perhaps sparking some ideas for the future of proof repair.

It's totally cool if you don't enjoy my work on proof repair, also, even though the power dynamic is weird because I'm teaching the class. I won't hold it against you, I promise; I will consider any feedback you have to make it better, too. But if you do enjoy my work on proof repair, I'd love to talk to you about some of your ideas, and maybe we can work together!

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. PUMPKIN Pi is implemented as a plugin for Coq. What do you think the tradeoffs are of implementing automation like this using a plugin, versus any other kind of automation we've seen so far in this class?
2. This approach to proof repair operates over low-level proof terms, rather than over high-level proof scripts. Do you think that it is possible to implement a useful proof repair tool that operates directly over proof scripts? Why or why not?
3. How would you go about extending a tool like this to handle more general classes of changes?
4. What would it take to convince you to use a tool like this in day-to-day proof development? Are there any features missing that you wish a tool like this had?
5. The future work section very briefly discusses the possibility of using machine learning tools to improve the performance of the decompiler. Suppose you are instead tasked with implementing a machine learning tool for proof repair from scratch, any way you like. How would you go about doing this?
6. How would you extend a tool like this to automatically repair the implementations of custom tactics?
7. Do you think any of the ideas presented here could be useful for program repair as well? And do you think any ideas from program repair could be useful for proof repair?
8. Write a paragraph responding to someone else's comment in the discussion forum.
9. 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.