Automata

Exhaustively verifying concurrent systems by turning "always eventually" into an automaton, and the state-explosion wall.

A language is regular iff it has finitely many distinguishable prefixes; and this gives you the unique minimal DFA.

Two very different-looking formalisms, exactly the same power. Explains how a regex engine really works.

Four grammar classes, four machine classes, one ladder. Why you can't parse HTML with a regex, stated as a theorem.