4 ms·
The presentation addresses this in a way. The argument is that in Coq you can write proof _scripts_ ("repeat this simplification operation until it does nothing
by mauricioc 9y ago
The presentation addresses this in a way. The argument is that in Coq you can write proof _scripts_ ("repeat this simplification operation until it does nothing", "pattern match on this definition and apply this operation to every subcase", "proof tactics" and so on), and in this way the same proof script can prove different theorems.
So there is a possibility that changing the code only forces you to change theorem statements (that is, the spec), allowing reuse of the proof script itself. Now you are doing software engineering on proof scripts, and you face the same generality/flexibility problems you would face when writing unit tests. A well-written proof script would be flexible enough, and a hacky one would lock things down too much.
- bsaul 9y agoThat part made me wonder if a day will come where some generic script would be able to work with any theorem on any code, maybe with the help of some kind of introspection ( at this level of abstraction i’m not even sure introspection is the right concept).
- deleted 9y ago[deleted]
- firethief 9y agoShort answer: no. Long answer: https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_... There cannot be a program that can prove (or even help a human to prove) any true statement about programs written in a Turing-complete language.
- bsaul 9y agoAs always with this theorem it's pretty hard to be sure if the kind of non provable statement happen often enough to be a concern in practice
- hackinthebochs 9y agoBut most code isn't using the features that make Turing complete languages messy, i.e. evolving the executable code as executing progresses. Most real-world code exists in a subset of Turing complete languages where generic theorem proving could probably work.