The Grand Unification
In 1934, Haskell Curry noticed something strange. In 1969, William Howard formalized it. They discovered that Logic and Computation are actually the exact same thing looked at from two different angles.
The Comparison
The isomorphism (meaning “equal shape”) states that:
- A Proposition (statement) in logic is a Type in programming.
- A Proof of that proposition is a Program of that type.
| Logic | Programming |
|---|---|
| Implication ($A \to B$) | Function Type (A -> B) |
| Conjunction ($A \land B$) | Product Type (Tuple/Pair (A, B)) |
| Disjunction ($A \lor B$) | Sum Type (Union/Either `A |
Why It Matters
Using this principle, we can build languages like Coq or Agda that allow you to write a program and mathematically prove it has no bugs. If the code compiles, the proof is valid.
Conclusion
The Curry-Howard Isomorphism is the bridge that reminds us that programming is not just “telling a computer what to do”—it is the literal application of mathematical logic.
References & Further Reading
- Philip Wadler: Propositions as Types
- Computerphile: Curry-Howard Isomorphism Video
- Stanford Encyclopedia of Philosophy: Type Theory
Last updated on