In constructive logic, a proof of "A or B" consists of a pair (T,P). If T equals 0, then P proves A. If T equals 1, then P proves B. This directly corresponds to tagged union data types in programming. A "Float or Int" consists of a pair (Tag, Union). If Tag equals 0, then Union stores a Float. If Tag equals 1, then Union stores an Int.

In classical logic, a proof of "A or not A" requires nothing, a proof out of thin air.

Obviously, we want to stick with useful data structures, so we use constructive logic for programming.

▲

pron an hour ago | parent | next [-]

> Obviously, we want to stick with useful data structures, so we use constructive logic for programming.

I don't know who "we" are, but most proofs of algorithm correctness use classical logic.

Also, there's nothing "obvious" about what you said unless you want proof objects, and why you'd want that is far from obvious in itself.

	▲	zozbot234 an hour ago \| parent [-]
		The difference only becomes evident when proving liveness/termination (since if your algorithm terminates successfully it has to construct something, and it only has to be proven that it's not incorrect) and then it turns out that these proofs do use something quite aligned to constructive logic.

▲

layer8 2 hours ago | parent | prev [-]

You aren’t giving any justification why proofs should necessarily map to data structures.

▲

amavect 2 hours ago | parent [-]

Not necessarily, I only argue for utility. You can find better justification in the Curry-Howard correspondence.

	▲	pron an hour ago \| parent [-]
		How have you used the Curry Howard correspondence to make proving the correctness of non-trivial algorithms easier (than, say, Isabelle/HOL or TLA+ proofs)?