Soffio

Summary

This article explores the Curry-Howard correspondence, a profound connection between type theory and mathematical logic where types are propositions, programs are proofs, and evaluation is proof normalization.

Key Concepts:

  1. Fundamental Mappings:

    • Implication (P ⇒ Q) ↔ Function types (A → B)
    • Conjunction (P ∧ Q) ↔ Product types (A × B)
    • Disjunction (P ∨ Q) ↔ Sum types (A + B)
    • Universal quantification (∀x.P) ↔ Dependent products (Πx:A.B)
    • Existential quantification (∃x.P) ↔ Dependent sums (Σx:A.B)

  2. Lambda Calculus & Logic:

    • Simply typed lambda calculus corresponds to intuitionistic propositional logic via natural deduction
    • Each typing rule is an inference rule; each program is a constructive proof
    • Classic combinators (K, S) prove logical theorems

  3. Intuitionistic vs Classical Logic:

    • Curry-Howard works for intuitionistic logic (constructive proofs)
    • Law of excluded middle and double negation elimination not universally provable
    • Ensures all proofs are constructive and computable

  4. Dependent Types:

    • Enable expressing first-order logic in types
    • Vector types prove properties like length preservation in append
    • Used in proof assistants: Coq, Agda, Lean, Idris

  5. Linear Logic & Linear Types:

    • Resources used exactly once
    • Rust's ownership system inspired by linear types
    • Session types ensure protocol correctness at compile time

  6. Practical Applications:

    • CompCert: Formally verified C compiler with correctness as a proven theorem
    • seL4: Verified microkernel with proven security properties
    • Smart Contracts: Type-level verification of financial invariants
    • Type-Safe Queries: Database libraries that prove query correctness

  7. Philosophical Implications:

    • Programs are mathematical objects
    • Correctness is compositional through types
    • The uncomputable corresponds to the unprovable (Gödel's theorems)
    • Type signatures are theorems; implementations are proofs

Profound Insight: The Curry-Howard correspondence reveals that programming and mathematics are not separate disciplines but unified—every well-typed program is a theorem, every proof is an algorithm. This perspective enables verified software where "it compiles" genuinely means "it's correct."

Impact: From verified compilers and operating systems to formally proven cryptographic implementations, Curry-Howard is transforming how we build reliable software, making the dream of mathematically proven correctness a practical reality.