3 ms·
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 d
by tlringer 7y ago
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.
- tom_mellior 7y agoGood 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.