  The Curry-Howard correspondence has made intuitionistic natural  deduction part of the computer science curriculum: it gives a  computational semantics for intuitionistic logic in which  computations, and the executions of programs more generally, are  effected through normalization. A proof of an implication  A ⊃ B, say, is a program that  converts data of type A into an output of type B.  The construction of an object (proof, function, program) f  of the type  A ⊃ B ends with an  abstraction. When an object a of type A is fed into f as an argument, the resulting expression is not normal,  but has a form that corresponds to an introduction followed by an  elimination. Normalization now is the same as the execution of the  program f. The use of intuitionistic logic is not tied to  any intuitionistic philosophy of mathematics, but is just a  systematic guarantee for the termination of the execution of computer programs.