Comment by zozbot234
19 hours ago
> My point isn't that most algorithm/program proofs need the excluded middle, it's that they don't benefit from not having it, either.
Because if they benefited from it (in surfacing computational content, which is the whole point of constructive proof) they'd be comprised within the algorithm, not the proof.
> in surfacing computational content, which is the whole point of constructive proof
The point of a constructive proof is that the proof itself is in some way computational [1], not that the algorithm is. When I wrote formal proofs, I used either TLA+ or Isabelle/HOL, neither of which are constructive. It's easy to describe the notion of "constructive computation" in a non-constructive logic without any additional effort (that's because non-constructive logics are a superset of constructive logics; i.e. they strictly admit more theorems).
[1]: Disregarding computational complexity
> When I wrote formal proofs, I used either TLA+ or Isabelle/HOL, neither of which are constructive.
True, but this requires using different formal systems for the algorithm and the proof. Isabelle/HOL being non-constructive means you can't fully express proof-carrying code in that single system, without tacking on something else for the "purely computational" added content.
That's not true. Non-constructive logics are extensions of constructive logics. You can express any algorithm in TLA+, and much more than algorithms.
You are right that when using non constructive logics, it's not guaranteed that the proof is executable as a program, but that's not a downside. Having the proof be a program in some sense is interesting, but it's not particularly useful.
3 replies →