Appendix D — Style Summary (one page) ·

The book in one page. Each rule has a chapter; each rule is checked by something.

# Claims

Every word declares its stack effect — and the declaration is true (ch. 2).
Ranges live in subtypes; choices live in enums; groupings live in structs (ch. 3).
Contracts are arithmetic about the values in view: no tautologies, no effects, no drift (ch. 4). Write them the way the prover will want them.
Declare what a word does (performs) and what it needs granted (requires); the caller decides (ch. 5).
Beyond two or three stack items, name them (=>) (ch. 2, 9).
Recursion is net-zero per level or it is rejected — keep it that way (ch. 6).
One writer or many readers, never both; a borrow’s life is its bracket; custody moves and is never cloned (ch. 7).
Hardware is named, never addressed; the descriptor wins every disagreement (ch. 8).

Factor until every word passes the one-sentence test; stop before shims (ch. 9).
Factor along the grammar: predicates keep their subject, loop bodies are net-zero, locked sections stay inline (ch. 5, 9).
A module’s .def is its constitution: exports are decisions, the mirror never drifts (ch. 10).
A shared resource is a declared resource, and the lock is bought only where reachability demands it (ch. 11).
A worker’s quotation carries its annotation; a join lives under its discharge (ch. 12).

If a fact is load-bearing, it is not a comment (ch. 1).
Checked failures are the cheapest failures: trap codes are verdicts, not embarrassments (ch. 1).
A proof states its boundary. Say what is proven, what is not, and which workstream closes it (ch. 6, 11, 13).
The mirror, the wall, and the seal are one mechanism: promises live in interfaces, interfaces are hashed, and hashes are refused on mismatch (ch. 10, 13).

Everything claimed, the machine checks; claims are cheap, and lies are loud.
Safety is not the brake — it is the engine: the rigor licenses the daring parts.