Well, to translate my words to your liking: "In my opinion, everyone already uses a sort of constructive logic for programming."

I challenge you on "most proofs of algorithm correctness use classical logic". That means double negation elimination, or excluded middle. I bet most proofs don't use those. Give examples.

▲

pron an hour ago | parent | next [-]

Oh, if you mean that most algorithm correctness proofs are finitary and therefore don't need to explicitly rely on the excluded middle, that may well be the case, but they certainly don't try to avoid it either. Look at any algorithm paper with a proof of correctness and see how many of them explicitly limit themselves to constructive logic. 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.

▲

zozbot234 an hour ago | parent [-]

> 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.

▲

pron an hour ago | parent [-]

> 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

	▲	zozbot234 42 minutes ago \| parent [-]
		> 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.

▲

zozbot234 2 hours ago | parent | prev [-]

Proofs of safety are proving a negative: they're all about what an algorithm won't do. So constructivism is irrelevant to those, because the algorithm has provided all the constructive content already! Proofs of liveness/termination are the interesting case.

You might also add designing an algorithm to begin with, or porting it from a less restrictive to a more restrictive model of computation, as kinds of proofs in CS that are closely aligned to what we'd call constructive.