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