The Curry-Howard Correspondence Appreciation Thread 🫶

YESSS this thread was so needed. ok my favourite elementary example: the identity function as the proof of A ⊃ A. in Haskell:

-- The proposition:  A implies A
-- The program:      identity function
identity :: a -> a
identity x = x

-- Conjunction intro: if you have A and B, you have A ∧ B
-- The program:       tuple construction
conj_intro :: a -> b -> (a, b)
conj_intro x y = (x, y)

-- Modus ponens: from (A → B) and A, derive B
-- The program:  function application!
modus_ponens :: (a -> b) -> a -> b
modus_ponens f x = f x  -- this is just ($) lol

the fact that function application IS modus ponens never gets old to me. every time you write f x in Haskell you're performing a logical inference step. you've been doing formal logic this whole time!!! 🤯

obligatory Wadler quote drop (he wrote a legendary paper on this):

also i want to highlight something OP's table hints at but doesn't spell out: the three-way extension. Lambek showed in the early 1970s that this isn't just logic ↔ types — it extends to cartesian closed categories. so we have a genuine trinity:

this is sometimes called "computational trinitarianism" 🙏 the three perspectives illuminate each other — a categorical construction tells you something about types, which tells you something about proofs, which tells you something about categories, round and round forever 🌀

voted "Categories ↔ Logic" in the poll obv

i have a lot of feelings about this. let me dump some of my favourite "oh wait it's all the same" moments:

1. Absurdity elimination = Empty pattern match

in logic, from ⊥ (False) you can derive anything (ex falso quodlibet). in Haskell, the empty type Void lets you write:

import Data.Void

-- "From False, derive anything"
-- absurd :: Void -> a
absurd :: Void -> a
absurd x = case x of {}  -- no cases! because Void has no inhabitants

2. Curry-Howard for classical logic

this one melted my brain a little. classical logic (with double-negation elimination) corresponds to continuations / call-cc. the Peirce's law ((A → B) → A) → A corresponds to call-with-current-continuation. Griffin discovered this in 1990 and i will never fully recover.

3. Proof normalization = beta reduction = computation

when you reduce a lambda term ((\x -> x + 1) 5 becomes 6), you're not just computing — you're simplifying a proof tree. Gentzen's cut-elimination theorem (a fundamental result in proof theory) and beta reduction in the lambda calculus are literally the same operation seen through the isomorphism 🤯

the Griffin result is SO good. classical logic gets continuations, linear logic gets session types / resource-aware computation, intuitionistic logic gets pure functional programs... it's like each logical system is secretly a programming paradigm dressed up as epistemology 😭

speaking of linear logic — can we talk about how linear logic ↔ linear types is an entire extension of the correspondence? Girard's linear logic with ⊗ (times), & (with), ⊕ (plus), ⅋ (par) maps onto linear type systems where resources must be used exactly once. this is how you get Rust's borrow checker from a logical perspective — it's literally linear logic enforced at compile time!!

the chain goes: Girard invents linear logic for theoretical reasons → Curry-Howard says it should correspond to a type system → Rust (and others) implement exactly those type system ideas → you get memory safety without garbage collection. the philosophy predicted the engineering 🌸

adding an Agda snippet because dependent types make the correspondence so explicit you can almost taste it:

-- In Agda, propositions literally ARE types
-- and proofs literally ARE values

data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x

-- Symmetry of equality is a PROGRAM that takes
-- a proof (p : a ≡ b) and returns a proof (b ≡ a)
sym : {A : Set} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

-- Transitivity IS function composition
trans : {A : Set} {a b c : A}
       → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

there's something almost spiritual about the fact that refl (the proof that anything equals itself) is literally the only constructor of the identity type, and pattern matching on it in sym is the entire proof of symmetry. the structure of the program is the structure of the proof.

also going to plug: Software Foundations (Pierce et al.) develops this entire correspondence formally in Rocq/Coq. extremely good if you want to see a real proof assistant built on these principles. free online! 🐱

something i always bring up with beginners: the "why does this matter for actual programming" question. type-checking IS proof-checking. full stop.

from Coq/Rocq's documentation (paraphrasing): because propositions are just types and proofs are just terms, checking that a proof is valid just amounts to type-checking the term. type checkers are relatively small, tractable programs — so the "trusted computing base" for a proof assistant can be tiny. you only need to trust the type checker!

this is why formally verified software (seL4 microkernel, CompCert compiler, etc.) is possible at all. the mathematical foundation is the Curry-Howard correspondence.

favourite correspondence expansion table (the "so what" version):

(yes I put "unit test = weaker form of witness" specifically to start drama in this thread)

ok i want to add the historical angle because I love it. the story is roughly:

🐱 1934 — Curry notices that the axioms of combinatory logic look suspiciously like the axioms of Hilbert-style propositional logic. observes the type-theoretic analogue but doesn't publish it formally until later.

🐱 1969 — Howard writes an influential (unpublished!) manuscript showing that natural deduction proofs directly correspond to typed lambda terms via an explicit structural isomorphism. it circulates for years before formal publication in 1980.

🐱 early 1970s — Lambek independently shows that the proofs of intuitionistic propositional logic and combinators of typed combinatory logic share a common equational theory: the theory of cartesian closed categories. this completes the trinity.

what i love is that Howard's manuscript wasn't even published when it started influencing everything. it was just passed around informally. mathematical gossip as the foundation of modern type theory 🫶

last one from me for now (have to go touch some theorems) — my favourite compact demonstration of the whole thing in Haskell using parametricity:

-- The composition operator (.) proves transitivity of implication!
-- (b → c) → (a → b) → (a → c)
-- i.e. "if B implies C, and A implies B, then A implies C"
(.) :: (b -> c) -> (a -> b) -> (a -> c)
(f . g) x = f (g x)

-- The const function proves "A implies (B implies A)"
-- i.e. any true thing can be proven from any hypothesis
const :: a -> b -> a
const x _ = x

-- `flip` proves the commutativity of antecedents:
-- (a → b → c) → (b → a → c)
flip :: (a -> b -> c) -> b -> a -> c
flip f y x = f x y

the Haskell Prelude is secretly a book of tautologies 🌸 every polymorphic function in there is simultaneously a proof of a theorem in intuitionistic propositional logic. go look at the type of curry and uncurry sometime and tell me you don't feel the universe winking at you.

anyway, thread is open. please drop more examples, more connections, more love for this beautiful correspondence. it's why i got into type theory and I just want everyone to feel the joy 🫶