Constructive proofs as programs

Published: Dec. 22, 2019, 5 a.m.

We consider the basic idea of the Curry-Howard isomorphism, that constructive proofs are essentially programs, and vice versa.\xa0 Several simple examples.\xa0 Why the law of excluded middle is not a legal constructive proof.