3 ms·
If 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 doe
by Retra 10y ago
If 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?