Module 19 — PL theory & type systems
Every chapter: first principles, What insiders know, a See it yourself lab, connections, and a quiz with worked answers.
The lambda calculus: the minimal machine
Three reduction rules, Turing completeness, the halting problem arriving in the same box — why every language is sugar on this.
Types as theorems, programs as proofs
Soundness = progress + preservation; Curry-Howard; null, generics, and subtyping as points on the guarantee frontier.
Memory safety as a theorem
The borrow checker as an affine type system; every module-01 language placed on the safety proof spectrum; where "unsafe" holes live.
GC as proof search
Liveness as the theorem, tracing as proof search, write barriers as monotonicity, pauses as proof cost — all collectors re-derived.
What types cannot do
Termination, spec fidelity, integer overflow, and the soundness/expressiveness trades — why bugs survive in safe languages.