Class 13: Mixed-Methods Verification

This class, we will read Computing Correctly with Inductive Relations [PDF] [DOI] by Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos.

This paper nicely brings together ideas from property-based testing (in the style of QuickCheck) with other important ideas from verification, and uses it to build really cool automation. I think it's a great example of how testing and verification can each enrich the other. Plus it's a cool application of Ltac2.

You can find a reading guide and the discussion questions below. A public version 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.

If you're pressed for time and read any two things, I recommend the introduction, the first example, and the evaluation (Sections 1, 2, and 6). The introduction is honestly one of the best I've read.

It's very normal not to understand all of the details of the core technical parts of this paper, like Sections 3, 4, and 5. They are still worth a read, but I would not stress too much if the details are hazy.

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 think a tool like this would be useful in an educational setting, for students learning Coq? What about for proof engineers developing large verified systems? If not, why not, and if so, how?
2. Do you think a tool like this could be useful to other proof automation (for example, a machine learning tool for proofs)? If not, why not, and if so, how?
3. Can you think of other possible producers besides those listed in the paper?
4. This paper is one example of how ideas from testing and proof automation can work nicely together. What other ways do you think testing and proof automation can work nicely together? It's OK to be speculative.
5. What do you think about the automatically generated checkers? Why do you think the authors choose to generate checkers that do not quite match the naturalness of the human-written ones? Can you think of any way to make the automatically generated checkers more natural in at least some situations?
6. Write a paragraph responding to someone else's comment in the discussion forum.
7. Write a list of any terminology or concepts you'd never heard of before reading this paper.
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.