3 ms·
It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.
by Retra 10y ago
It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.
- mafribe 10y agoI'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in LCF provers using HOL as a logic. Are you saying that the guarantees of correctness are not in themselves useful? [1] https://cakeml.org/ https://cakeml.org/ [2] https://sel4.systems https://sel4.systems
- Retra 10y agoIf I write a program X and tell you it was proven correct, do you know that X is useful? To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation. Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)
- mafribe 10y agoI'm not sure what you mean. We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main difference is that HOL-based provers like Isabelle/HOL has classical built in from the start -- all proof automation supports classical reasoning. Constructive reasoning eschews classical methods. In order to prove the correctness of a program X, I need a specification S, and then I construct a proof P that X |= S, i.e. that X satisfies the specification S. I use an interactive proof assistant to check the proof P. There is no disadvantage that I can see if the proof P of X |= S is classical, at least from the point of view of program correctness. Maybe you mean something else?