Resolution and CDCL
SAT is NP-complete (The Cook–Levin theorem) yet solvers handle millions of variables.
L2
Register Allocation Is Graph Coloring
A named theory result sitting in the middle of every compiler backend, plus why the NP-hardness does not stop anyone. Part V's counterweight to all the type theory.
Hoare Logic and Weakest Preconditions
Reasoning about programs as a proof system; loop invariants as the hard part, and why they can't be inferred in general.
Codd's Theorem
Relational algebra and relational calculus have equal expressive power. Why SQL is declarative and why a query planner can exist at all.
Parametricity: Theorems for Free
A polymorphic type alone tells you what the function must do. can only permute.
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 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.
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.
The Exponential Time Hypothesis and Fine-Grained Complexity
Beyond P vs NP: why your O(n^2) string algorithm is probably optimal too.
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.
Vector Clocks and Causal Consistency
Detecting concurrency exactly, at the cost of O(n) metadata. The tradeoff every eventually-consistent store makes.
Parameterized Complexity (FPT and W[1])
"NP-hard" hides that some hard problems are easy when one parameter is small. The most practically useful refinement of Karp's 21 problems.
Approximation Algorithms and Ratios
The positive side: 2-approximate vertex cover, PTAS, and where the approximability cliff sits.