The language stack : from silicon to semantics

It is 2026, and a language model can generate a lexer, a type
checker, and a working compiler in seconds. So why learn to build
them by hand? Because a generated artifact is an assertion -
and an assertion you cannot evaluate is not knowledge, it is a hope
with good syntax. The value was never in the typing.

This book carries one language - Lark, the Lambda Affine Resource
Kernel - from a real instruction set to a machine-checked proof
that its meaning is sound, treating the hardware, the theory, and
the proof as a single argument. You begin at the silicon and build
upward through lexer, parser, type system, interpreter, and
optimizer, to a code generator that runs Lark as native code on an
affordable Raspberry Pi Pico 2/2W.

Theory is earned, not assumed: Hindley-Milner inference, affine
ownership, and traits, each introduced when the implementation needs
it. And the book teaches the discipline that code-generating tools
demand - an interpreter that defines what a program means,
a differential-testing harness that says which back end is wrong, a
type-safety theorem that bounds what any transformation may do. And
then it turns that machinery on itself: the finished compiler is
fuzzed, the tests are checked with planted bugs, and even the proof
kernel is attacked until it gives up its own flaws - because a
guarantee is worth exactly as much as the adversary it has survived.

For the technically literate programmer who has always meant to
understand what is under their language and never found the entry
point. It assumes familiarity with Python or C and basic data
structures - but not a line of compiler theory.