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.