Parametricity: Theorems for Free
A polymorphic type alone tells you what the function must do. can only permute.
Posts
IP = PSPACE
Interaction plus randomness lets a prover convince you of things you could never check alone.
Progress and Preservation
"Well-typed programs don't go wrong", stated as the two lemmas that actually prove it. What a type system does and does not promise.
Hindley–Milner and Principal Types
Every typable term has one most general type, and it's inferable. Why ML and Haskell need so few annotations, and why subtyping breaks it.
The Curry–Howard Correspondence
Programs are proofs, types are propositions, evaluation is proof simplification. The most beautiful idea in the series.
The Lambda Calculus and the Y Combinator
Three rules, all of computation, and recursion built from nothing. Absorbs Church–Rosser confluence: reduction order doesn't change the answer.
The CALM Theorem and CRDTs
A program can be coordination-free iff it's monotone. The positive result hiding behind all the impossibility ones.
The CAP Theorem and PACELC
What it actually says, why it's routinely misquoted, and why latency (the "ELC") is the part that governs real designs.
Paxos, Raft, and the Shape of Consensus
How real systems dodge FLP impossibility: safety always, liveness only when the network cooperates.
Quorum Intersection (R + W > N)
One inequality generating the entire read/write consistency tradeoff space.
The Myhill–Nerode Theorem
A language is regular iff it has finitely many distinguishable prefixes; and this gives you the unique minimal DFA.
Kleene's Theorem: Regexes Are Finite Automata
Two very different-looking formalisms, exactly the same power. Explains how a regex engine really works.
BPP, Pseudorandomness, and Derandomization
Randomness probably doesn't add power; the surprise is that hardness is what buys you fake randomness.
The Exponential Time Hypothesis and Fine-Grained Complexity
Beyond P vs NP: why your O(n^2) string algorithm is probably optimal too.
Parity Is Not in AC^0
An actual, unconditional circuit lower bound. Proof that lower bounds are possible at all, which is what stops The barriers: relativization and natural proofs from...
The No-Cloning Theorem
An unknown quantum state cannot be copied, and the two-line proof is just linearity.
The Nyquist–Shannon Sampling Theorem
Sample above twice the bandwidth or lose information irrecoverably.
The Byzantine Generals Problem
You need 3f+1 nodes to tolerate f liars, and that bound is tight.
FLP Impossibility
No deterministic consensus in an asynchronous system with one crash fault. The rigorous theorem that CAP only gestures at.
Vector Clocks and Causal Consistency
Detecting concurrency exactly, at the cost of O(n) metadata. The tradeoff every eventually-consistent store makes.