Resolution and CDCL
SAT is NP-complete (The Cook–Levin theorem) yet solvers handle millions of variables.
Logic
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.
The Curry–Howard Correspondence
Programs are proofs, types are propositions, evaluation is proof simplification. The most beautiful idea in the series.
The Barriers: Relativization and Natural Proofs
Why P vs NP has resisted for fifty years, stated as two theorems about which proof techniques cannot work.
The Cook–Levin Theorem
SAT is NP-complete: circuits encode computation. The technical heart of the whole field.
Godel's Incompleteness Theorems
Any sufficiently strong consistent system has true statements it can't prove, and can't prove its own consistency.
Kleene's Recursion Theorem
Any program can obtain its own source. Quines aren't a party trick; self-reference is guaranteed by the model.
The Halting Problem
No program decides termination for all programs. The ancestor of every other undecidability result.
Cantor's Diagonal Argument
Some infinities are bigger; there are more problems than programs. The proof technique that The Halting problem and Godel's incompleteness theorems both reuse.