compilers

Two landmark systems carry machine-checked proofs of real code: a C compiler and an operating system kernel. Their published effort figures give the honest price of full verification, and their trusted computing bases show exactly what a proof still leaves unproved. This lesson uses both to decide where verification pays.

Correct gradients are useless if computing them exhausts memory. Radiative backpropagation, path replay backpropagation's constant-memory trick, and why differentiable renderers needed their own compiler.

The parser only checks syntax — it happily accepts `x = y + z` even if none of those names exist. Semantic analysis adds meaning: it builds symbol tables, resolves names, enforces scoping rules, and runs the type checker that catches the errors a grammar cannot. Learn what happens between the raw AST and the typed AST the IR generator gets.

The parser takes a flat token stream and recovers the hierarchical structure the programmer intended. Learn context-free grammars, recursive-descent parsing, operator precedence, the difference between a parse tree and an AST, and when LL versus LR parsers matter — including the classic dangling-else ambiguity.

Before a compiler can understand your code it has to chop it into meaningful pieces. Learn how scanners work, how regular expressions become finite automata, why maximal munch is the rule, and what a real token stream looks like — the foundation every later compiler phase depends on.

The typed AST is high-level — too high for a CPU. Learn why compilers lower to an intermediate representation first, what SSA form buys you, how classic optimizations (constant folding, dead-code elimination, CSE) transform IR, and how instruction selection and register allocation finally produce machine code.