Part V — The language
AIR: a language whose
first requirement is repair
Chapter 18
A first program
It sums the squares of the even integers below n. Read it once, then notice what is not there.
There is no loop. Nothing says how many times anything happens, or in what order, or on how many cores. There is no accumulator being updated, because there is no update — every name is bound once. There is no integer width buried in a default, no overflow rule you have to know, and no comment explaining an assumption.
Everything that would have lived in someone’s head is on the page.
fn sum_squares_even(n: exact_i64) -> exact_i64
requires n >= 0
effects none
{
%range = range 1, n
%evens = filter %range where even
%squares = map %evens with square
%total = reduce %squares using add identity 0
ordering free parallelism permitted overflow trap
return %total
}$ air run sum_squares_even.air --n 100
161700Line by line
fn sum_squares_even(n: exact_i64) -> exact_i64The signature
exact_i64 is not i64. It is a 64-bit integer with exactness as part of the type — arithmetic on it either produces the mathematically correct answer or fails.
requires n >= 0The contract
A precondition. The toolchain proves it at every call site where it can, and compiles a guard where it cannot. Either way it is recorded in the artifact.
effects noneThe effects
Reads no files, opens no sockets, mutates nothing, consults no clock. Declared, checked against the body, and at run time enforced by giving it no capabilities to violate.
%total = reduce %squares using add identity 0The computation
Those % names are not variables — nothing is ever assigned twice. They are identities, and they are what makes repair local rather than global.
ordering free parallelism permitted overflow trapThe freedoms
Two grants and a constraint. The compiler may reorder and may parallelise; on overflow it must fail rather than wrap. Without that line the compiler would have to ask. With it, it knows.
What the compiler does with it
Nothing in that program says “loop”, and the obvious implementation is one. The four operations get fused — %range, %evens and %squares are never built, because nothing requires them to exist as data.
int64_t total = 0;
for (int64_t x = 1; x < n; ++x)
if ((x & 1) == 0)
total += x * x;That decision appears nowhere in the AIR. It is legal because the operations are pure and because the program granted ordering free. The author committed to meaning; the compiler committed to strategy. That division is the architecture the whole book argues for.
Chapter 21 — if you read one chapter, read this
A protocol between the compiler and the generator
An error message is addressed to a reader. It is prose, it is allowed to be witty, and its quality is judged by whether a person felt helped. The record below is addressed to a program. What comes back from it is not a feeling but a next action.
What most languages report
TypeError: unsupported operand type(s) for +: 'int' and 'str'That names a symptom, at a location that moves, with no indication of what would satisfy it or how much may be changed. It is a fine message for a person. For a producer it supplies one usable fact and leaves four questions open.
What AIR reports
diagnostic {
code E-CONTRACT-017
fragment %total
obligation associative(add)
status unproven
expected a combining operation with a declared identity
found add, identity undeclared
legal exact | tree | relaxed(error <= e)
repair_scope %total
dependencies []
checked [ parse ok, types ok, effects ok, contracts partial ]
}status
Distinguishes unproven from false — the field nobody emits. Unproven means the toolchain could not establish it and it may well be true. False means the fragment needs replacing. A producer that cannot tell them apart wastes its next attempt on the wrong move.
legal
Enumerates the answer set. Where a rule admits a finite set of options, listing them turns an open-ended repair into a choice — enormously cheaper than making the producer rediscover the rule.
repair_scope
Says how much of the program may be touched. Nobody emits this either, and it is the difference between a patch and a regeneration.
“A message can be reworded to read better in a patch release. A protocol field cannot — something is parsing it. That is why code is stable.”
Anyone building a coding agent can adopt this record next week, against Python or Rust or anything else, without writing a line of AIR. It is also the cheapest item on the falsification list in Chapter 27: emit both forms from the same compiler and compare the repairs.
What happened when that was measuredThe rest of Part V
Values and Types
Exactness as part of the type, not a library convention.
Fragments, Identity and Repair
Names that survive an edit, so a fault can point at something stable.
Effects and Capabilities in Practice
Declared, checked, and enforced by withholding what was never granted.
Contracts
Proved where possible, guarded where not, recorded either way.
Freedom
What the compiler may choose, stated rather than assumed.
From Intent to Native Code
The whole path, through Clang, on your machine.
Calling the World
The boundary where declared effects meet an undeclared operating system.
Stated limits
Deliberately small
Appendix A.12 is explicit about the fragment of computation AIR covers today, which is smaller than a reader might assume from the argument around it. The book also acknowledges the verification-language tradition it draws on, and what generalising would cost.
“A language you can read in an afternoon is a language you can argue with. Everything about it is designed to be disagreed with in specifics and, I hope, agreed with in shape.”