The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, reveals a deep connection between computer programs and mathematical proofs.

This remarkable isomorphism shows that:

  • Types correspond to propositions
  • Programs correspond to proofs
  • Program execution corresponds to proof normalization

For example:

  • The type A → B corresponds to the logical implication A ⊃ B
  • Product types (A × B) correspond to logical conjunction (A ∧ B)
  • Sum types (A + B) correspond to logical disjunction (A ∨ B)

This correspondence has profound implications for both computer science and mathematics, suggesting that programming and mathematical proof are fundamentally the same activity viewed through different lenses.