Talia Ringer on Nostr: I had a really wonderful much-needed morning of pair proving in Coq with one of my ...
I had a really wonderful much-needed morning of pair proving in Coq with one of my PhD students. We have worked bottom-up for so long, so we are now working top-down from the theorem we want to what we need to get there (lemmas and then, as we get further down, definitions).
We got the main theorem proven, but the admitted lemmas rely on definitions we haven't fully defined yet. So now she can keep working downward to each lemma and ask if it's true, if it's what we need, and if the definitions are all set up to prove it or if she needs to fix those.
Then in another week, we'll rendezvous for another pair proving session. Even 90 minutes of pair proving can be wildly productive. At that point we can either keep working downward or, if breaking changes have occurred at the bottom, upward to repair the proofs.
It's fun because I can help a lot very quickly, and because I genuinely enjoy the process. But also because, as someone who builds tools for proof engineers, I really like seeing the proof engineering process in action and dissecting my thoughts and communicating them.
I think this back-and-forth process of bottom-up and top-down proving passes, this interplay between figuring out what to prove and figuring out how to prove it, discovering the former as you work through the latter and the latter as you work through the former---it's super cool. It's underexplored from both an automation perspective and a user interface perspective.
We got the main theorem proven, but the admitted lemmas rely on definitions we haven't fully defined yet. So now she can keep working downward to each lemma and ask if it's true, if it's what we need, and if the definitions are all set up to prove it or if she needs to fix those.
Then in another week, we'll rendezvous for another pair proving session. Even 90 minutes of pair proving can be wildly productive. At that point we can either keep working downward or, if breaking changes have occurred at the bottom, upward to repair the proofs.
It's fun because I can help a lot very quickly, and because I genuinely enjoy the process. But also because, as someone who builds tools for proof engineers, I really like seeing the proof engineering process in action and dissecting my thoughts and communicating them.
I think this back-and-forth process of bottom-up and top-down proving passes, this interplay between figuring out what to prove and figuring out how to prove it, discovering the former as you work through the latter and the latter as you work through the former---it's super cool. It's underexplored from both an automation perspective and a user interface perspective.