The language model: agnostic verbs, total by construction

The rule language is a closed vocabulary, not a programming language. Its expressiveness is fixed by design and grows only through vetting, never through runtime computation. Three laws govern it, and everything else - bindings, the extension tiers, the single external liability - is a consequence of holding those three.

---

The three laws

1. Every construct maps to a primitive, or it is rejected. A verb that is not one of the closed effects and not a named composition drawn from an imported module is a wish, not a mechanic. There is no “close enough”, no best-effort, no silent coercion. The same discipline that governs external imports - name where the behaviour comes from, or it does not run - is turned on the language itself. A parser, a linter, and the specification all check against one registry of primitives; if a construct is not in that registry, it is not in the language.

2. Verbs are unit-agnostic. A verb never bakes in a unit or a type. The verb is the operation; the operand’s type decides whether the operation is legal. You split a money, a percentage, an int, or a quantity - never a party or an opaque. price is not a verb, it is a money; there is no expect-price, only a comparison where both operands happen to be money. Each effect declares the operand types it accepts, and a type-physics pass rejects a verb applied to a type it does not accept - the same pass that already refuses “hours + kronor”. A fused, unit-specific verb like split-money is a design smell: the correct form is always an agnostic verb plus a typed operand.

3. Nothing crashes. Every evaluation halts in bounded time and bounded memory. No recursion, no unbounded loops (only a bounded map over a collection), immutable single-assignment bindings, effects only on declared state - so a rule cannot hang, stack-overflow, or exhaust memory. The only thing that grows is the append-only log, linear in events. The single liability surface is a host function: it can be wrong, slow, or absent, but its failure is a declared fault verdict, never a machine crash. Safety here is not a hope, it is decidability the linter proves - once recursion is banned, totality becomes a syntactic check.

How the vocabulary grows follows from law 1. Two routes only: a vetted module that composes existing primitives under a name (the cheap, default path), or a new core primitive admitted through a human vetting gate, and only when a real corpus proves no composition suffices. Expressiveness never grows by adding computation - no loops, no recursion, no clock, no floats, no runtime macros.

---

Bindings and lifetimes

The binding rules are borrowed wholesale from Rust’s ownership model, then made stricter.

let is immutable and single-assignment. A let binds a name exactly once. There is no mut, no reassignment, and - stricter than Rust - no shadowing: a name binds exactly once per scope, so a receipt trace never carries two bindings of the same name meaning different things. This is single static assignment, and it is what makes replay deterministic and totality a syntactic check.

let expected := rate-at(senior, line.period)
let expected := 900 SEK           # ERROR: `expected` already bound (no reassign/shadow)

Ownership is move / copy / borrow. move consumes - the source no longer holds the value, and use-after-move is a compile error (values are linear, spend-once). copy duplicates a freely-duplicable value and is receipted. borrow is a scoped read reference that cannot outlive its owner.

move money.escrow -> seller
move money.escrow -> buyer        # ERROR: use-after-move (escrow already consumed)

The borrow checker is a lint pass. It runs at genesis, at the same status as pool-safety and match-exhaustiveness. Ownership errors are caught before signing; they are decidable.

Two lifetime scopes:

• Intra-rule - let bindings live for one rule evaluation (or one line of a bounded iteration) and then die. Locals, exactly as in Rust.
• Inter-event - pool tokens and register rows are owned across events. A moved token is gone from the pool for every future event. This is ownership that persists through the log, not the stack frame.

---

The extension model

Expressiveness grows by composition, never by runtime computation. Two tiers are open; the third is refused outright.

Tier 1 - core plus vetted modules. Compose the closed primitive set. New primitives enter only through the human vetting gate.

Tier 2 - user-defined functions, fenced hard. A function is:

• never inline - it is a module, a separately governed and pinned library unit;
• total - no recursion, only bounded iteration, immutable bindings, so termination is a syntactic check;
• mandatory-tested - it ships with its own isolated tests and cannot be published, flattened, or signed with a failing or absent test. The discipline is stronger than the usual “tests exist” rule, because a consumer’s flatten re-runs those tests at their signing time. The tests are the documentation and the behavioural spec.

Tier 3 - arbitrary imported code - refused. The only external computation admitted is a host function: a machine-provided surface, not a user-shipped blob.

No recursion. General recursion is undecidable (the halting problem) and the crash vector; banning it makes totality syntactic. If a real corpus ever needs tree-walking, the only admissible form is structural recursion - recurse on a strictly smaller piece of a finite declared shape, with a checker-verified decreasing measure and a hard depth cap - added through the vetting gate, never before.

One signature grammar for every function. In-language and host functions rhyme; only the body differs (body: for in-language, host: / binding: for external).

function <name>:
  in:  { <field>: <type>, ... }     # a SHAPE: named, typed fields (never positional)
  out: <type>
  body: <expression>                # in-language, total-checked   -- OR --
  host: machine | binding: ...      # external liability, no body
  guards: <post-conditions on out>
  test "<name>": <name>(<field>: <val>, ...) == <expected>

Named arguments always. Inputs are shapes; calls bind by name - ranta(principal: X, rate: Y, days: Z), never positional - because unnamed arguments are where a signer loses the thread. The one exception is a small positional prelude - sum, avg, count, min, max, abs, clamp and the operators + - x / - where names would be noise. The prelude is a closed set, extended only through the vetting gate. Dividing prelude functions carry declared rounding, and type-physics restricts them to ordered operands (min/max) or additive ones (sum/avg) - never a party, opaque, or id.

---

Host functions

Domain math that is genuinely complex and moving - tax, freight rating, currency conversion - does not belong inside a signed contract. It enters as a host function: a capability the running machine exposes, declared as a dependency. Think of it as a syscall against a standardized ABI, not as imported code. It is the one liability the design accepts.

• Machine-provided, standardized. The contract declares host: machine, and any conformant host must provide the surface. (Bind it to one vendor instead and you pay a real portability cost.)
• Captured as a signed fact, replay-safe. At execution the machine computes the value once and writes the answer into the log as a signed fact. Replay re-reads the stored answer and never re-calls - a 2027 tax engine need not still exist in 2035 for the receipt to verify. The result is an input, not a live computation.
• Guarded, never blindly trusted. Post-conditions check the answer: a returned rate must be in the declared VAT set, cross-sums must conserve. A compromised host can stall a contract; it cannot mis-price one silently.
• Fault, not crash. Wrong, slow, or absent resolves to a declared fault verdict; the machine stays up.

There is an honest asterisk here. “Runs on its own, no external cord” holds for verifying and replaying a contract, not for advancing one through a host-computed step. The cord exists only at live execution of a host-touching event.