The Curry-Howard correspondence is the observation that logic and programming are, at a deep level, the same subject seen from two angles. A logical proposition corresponds to a type, and a proof of that proposition corresponds to a program whose type is that proposition. Philip Wadler’s paper “Propositions as Types” sets out this correspondence and argues that it is not a coincidence but a recurring structure that has been discovered independently many times.
The two names come from Haskell Curry and the logician William Howard, who each noticed pieces of the parallel: Curry observed that the types of certain combinators mirror the axioms of logic, and Howard extended the idea to a full correspondence between proof systems and typed lambda calculi. The Stanford Encyclopedia entry on type theory places this proofs-as-programs reading among the central themes of the field.
The practical payoff is that a type checker can act as a proof checker. If you can write a program that has a given type, you have, in effect, supplied a proof of the corresponding proposition. This is the foundation on which proof assistants like Coq, Agda, and Lean are built, where checking a proof and type-checking a program are literally the same operation.
For everyday functional programmers the correspondence explains why rich type systems feel like reasoning tools: writing well-typed code is a constrained form of constructing a proof, and many properties can be guaranteed simply by getting the types to line up.