The Limits of Computation: What No Program Can Do

Some things are not slow to compute, they are impossible, and the boundary is sharp enough to prove in a few lines. This path climbs the ladder of machines one memory model at a time: finite states and the counting argument that defeats them, then a stack, then an unbounded tape. At the top the limit stops being about memory and becomes the halting problem, generalised by Rice to every semantic property at once. The last lesson spends that result on why every type checker and verifier must choose which way to be wrong.