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