See https://codewords.recurse.com/issues/one/type-systems-and-logic https://codewords.recurse.com/issues/one/type-systems-and-lo... for a pretty elaborate respo

See https://codewords.recurse.com/issues/one/type-systems-and-logic https://codewords.recurse.com/issues/one/type-systems-and-lo... for a pretty elaborate response to this question. tl;dr: types are propositions and values are proofs of those propositions. Constructive logic is not concerned with (true xor false), but rather "I can prove A" or "I can prove not-A". There's also the middle ground of "I don't know how to prove anything about A".