Software Is a Guarantee Problem. The AG Tower Is a Guarantee Machine.

Here's a thing most engineers have stopped noticing: almost everything you do at work is a substitute for a proof you don't have.

You write unit tests because you don't have a proof. You add integration tests because unit tests miss interactions. You build staging environments because integration tests don't model real traffic. You pay for observability because staging lies. You run postmortems because observability missed it. You write runbooks because postmortems don't prevent recurrence. You hire SREs because runbooks don't execute themselves.

Each layer is an after-the-fact substitute for a before-the-fact guarantee.

---

The move

The move that has quietly defined the last 20 years of serious industrial programming — TypeScript at Stripe, Rust at AWS and Cloudflare, TLA+ at DynamoDB/S3/EBS, SMT-backed IAM at AWS, differential privacy, seL4, CompCert, OPA — is always the same move.

Pull a property from "things we hope to catch at runtime" into "things the compiler refuses to build without."

Cloudbleed and Heartbleed were unchecked-bounds bugs that cost the industry billions — both structurally impossible in a language that makes the bound part of the type. The Ariane 5 inquiry traced a $370M rocket loss to an unchecked float-to-int conversion. Knight Capital lost $440M in 45 minutes to a dead-code reactivation a type system would have flagged. The AWS TLA+ paper (Newcombe et al., 2015) ended the "formal methods don't scale" debate by finding subtle DynamoDB/S3/EBS bugs that months of fuzzing had missed. Differential privacy converted "is this release safe?" from a review meeting into a theorem with a tunable epsilon.

Every one of these is the same shape: an ambient, discipline-enforced property becomes a mechanically-checked property, and a whole class of bugs collapses.

The tower

I've been building an attribute grammar compilation tower that generalises the move. It's a substrate in which "thou shalt not X" is itself a composable, layer-by-layer specification: the refuse-ifs are grammar equations, and they propagate upward by construction. Each layer is one tree; each tree compiles into the next layer's source code; the seed compiles itself, byte-for-byte, at 141,358 bytes today.

The intellectual lineage is old and serious: Knuth 1968 (attribute grammars), Futamura 1971 (the partial-evaluation trick that turns an interpreter into a compiler), Smith 1984 (reflective towers of interpreters), Thompson 1984 (self-compiling compilers), Steele 1998 (languages that grow themselves from a small seed), Elliott 2017 (compiling the same spec into many target categories). Each thread has been vindicated in its own subfield. Putting them together and aiming them at real-world guarantees is overdue, not novel.

The vertical

The first application is data engineering — where the gap between the guarantees practitioners want and what their tools provide is widest, the diagnoses are already written (Kimball on grain, Codd on relational closure, Hellerstein on declarative dataflow, Brandon on SQL), and the cost of the status quo is paid in cash by every company that ships dashboards.

Every aggregation bug is a grain bug. Every reconciliation is a runtime confession that a compile-time guarantee was missing. Every lineage-overlay service is paying a very high operational cost to recover a property a compiler could hand them for free. The whole "data observability" category is the category-wide admission that correctness is only assessed after a wrong number has been published to a dashboard.

You shouldn't have to run it. You should be able to hand your pipeline to a compiler, and the compiler should refuse to build it if the grain is wrong, the reconciliation doesn't close, or the lineage contains an implicit cartesian product.

---

I wrote up the full case — the horizontal (every domain is a guarantee domain), the vertical (data engineering is 30 years behind), the intellectual lineage back to Knuth 1968, and a curated reading list — as a visual, interactive explainer with a clickable timeline, a grid of guarantee domains, and a side-by-side comparison of the SQL loop vs the Rust loop.

→ Read the full interactive explainer

The flashcards below are the TL;DR — the conceptual moves worth leaving the page with.