The book leans on a small vocabulary, some of it coined here. These are the important terms, with the chapter where each is developed.
The Central Arrangement
Term
Meaning
Tight core, open edge
The book's central arrangement: constrain the part that must be correct, open the part that must grow, and join them with a contract. (Ch 1, 14, 15)
Membrane
The contract at the seam between a constrained core and an open edge. It states the core's terms; the edge must meet them; trust flows one way, inward. (Ch 2, 9, 14)
Seam
Any place two parts of a system meet, or the system meets the world. The unit of the constrain-or-open decision — you decide seam by seam, not once for the whole system. (Ch 14)
Constraint tradition
The discipline of fighting wrongness by narrowing what the program can express — closing doors. (Ch 1)
Flexibility tradition
The discipline of fighting rigidity by arranging for growth by extension rather than edit — opening doors. (Ch 1)
Contracts
Term
Meaning
Design by Contract
Building specifications into code as require, ensure, invariant, and variant. The connective tissue of the book. (Ch 2)
Precondition (require)
What a caller must establish before invoking a routine; it moves an obligation across the boundary so the body may assume it. (Ch 2)
Postcondition (ensure)
What a routine guarantees on return. old e refers to the value of e on entry, letting a postcondition speak about change. (Ch 2)
Invariant
A property that holds across an object's whole lifetime (before and after every method), or is preserved across every loop iteration. (Ch 2, 3)
Variant
An integer that strictly decreases toward a bound each iteration, proving a loop or search terminates. (Ch 2, 13)
Constraining the Core
Term
Meaning
Sum type
A value that is exactly one of a fixed set of shapes; in Nex, written concisely with union, which expands to a sealed set of variant classes. (Ch 3)
Refinement type
An existing type narrowed by a predicate (declare type Quantity = Integer where n: n > 0); the value stays its base type, and the rule is checked wherever a value is narrowed in. (Ch 3)
Constrained type
A type carrying a rule its values always satisfy โ a refinement, or a class with an invariant โ so holders never re-check (e.g. a positive Quantity). (Ch 3)
Make illegal states unrepresentable
Arranging types so bad values cannot be constructed at all, rather than detected after the fact. (Ch 3)
Exhaustiveness
The compiler's guarantee that a match over a sealed type handles every case; a missing one is a compile error. (Ch 3)
Parse, don't validate
Converting untrusted input into a precise type once, at the boundary, so the result carries the proof and the interior never re-checks. (Ch 4)
Total function
A function that returns a valid result for every input its type admits, with no hidden exits (no thrown exception, no surprise nil). (Ch 5)
Functional core, imperative shell
Keeping domain logic pure and pushing all effects to a thin outer layer that performs them. (Ch 6)
Effects as data
Having the pure core describe effects as values (a to-do list) instead of performing them, leaving the doing to the shell. (Ch 6)
Composing and Opening
Term
Meaning
Combinator
A value in a closed algebra: primitives plus combining forms that return the same type, so results compose without limit. (Ch 7)
Closure property
The property that a combining form returns the same type it consumes, so its output can be its input — what makes a few parts an unbounded kit. (Ch 7)
Layering / stratified design
Composing behavior vertically: each stratum wraps the one beneath, adding one concern, and each is itself a complete version of the behavior. (Ch 8)
Substitutability
The obligation that a wrapper may add to a base's behavior but must not break the promise callers rely on — a contract, not a type. (Ch 8)
Additive design
Growing a system by writing new code, never by editing what already works. (Ch 7, 8, 9)
Generic operation
An operation whose behavior for a given kind is looked up in a runtime table, extensible by registration without editing the operation. (Ch 9)
Data-directed dispatch
Selecting behavior by looking up a runtime tag in a table, rather than by a fixed branch or a compiled method. (Ch 9)
Expression problem
The difficulty of adding both new data kinds and new operations over them without editing existing code; dissolved by putting the kind-to-behavior association in data. (Ch 9)
Domain-specific language (DSL)
A small language whose words are domain concepts; embedded (values in the host, compiler-checked) or external (its own syntax, parsed from text). (Ch 10)
Extensible evaluator
An interpreter with closed syntax but an open, runtime-extensible table of primitive operations. (Ch 11)
Partial Information
Term
Meaning
Propagator / cell
A network model of computation: cells hold partial knowledge; stateless propagators wake when a cell sharpens and spread the consequence. (Ch 12)
Partial information
A cell's content when it may know nothing, a range, an exact value, or a contradiction — not merely a value. (Ch 12)
Monotone merge
Combining two pieces of knowledge so the result is only ever sharper, never wider — what makes a network order-independent. (Ch 12)
Truth maintenance / provenance
Recording why a cell knows something, so a retracted premise cleanly removes what depended on it. (Ch 12)
Unification
Finding the substitution of unknowns that makes two structures identical, or failing. (Ch 13)
Logic variable / substitution
An unknown to be solved for, and the accumulating map from such unknowns to the terms they are bound to. (Ch 13)
Occurs-check
The guard that prevents binding a variable to a structure containing itself, keeping a substitution consistent. (Ch 13)
Search / backtracking
Trying a tentative assignment, checking it, and undoing it to try another when a later constraint fails. (Ch 13)