Hacker News Reader

Idea for getting "almost correct" proofs: Take a big Coq project like CompCert or whatever. Search the version control history for commits with small changes to definitions. These very likely come with corresponding changes to proofs as well. Now apply only the code changes but not the proof changes: You get a state with "almost correct" proofs and as a bonus known "ground truth" proofs as well.

View on HN

This is a really interesting idea. In some sense, you can say a proof script is "almost correct" if it proves a slightly different theorem.

I suspect the one difficulty there would be finding such incremental changes on Github. It was surprisingly difficult to find small changes to specifications in Git history for a different project that I did. Too many large commits and too much history revision, so you often lose the incremental changes. Still, it is worth trying.

Good point about the difficulty of finding incremental changes. Maybe it's better the other way round: Pick an arbitrary commit and only roll back the changes it introduces to one proof. This would model the situation where a programmer has just changed the code and is now setting out to adjust the proof.

Reply on news.ycombinator.com