# 04 — Behaviour and execution

## The distinction

The rule is **not** "no code." It is **no implicit execution**.

A unimsg document may represent behaviour: a formula, a lambda term, a WASM module, a
build derivation, a morphological rule, a query plan. What it may never do is cause any
of that to run as a consequence of being *read*.

> Decoding must be total, terminating, and side-effect free — always.
> Interpretation is a separate verb the host must explicitly invoke.

## Why the historical failures happened

Pickle, Java serialization, and `yaml.load` were not dangerous because they carried
behaviour. They were dangerous because **parsing was executing**. The reader asked for
structure and received arbitrary effects. Classic confused-deputy: the trust boundary
was in the wrong place.

XML's XXE and billion-laughs are the same error in a different costume — resolution and
expansion performed at parse time.

## Three verbs, three trust levels

| Verb | Operation | Cost | Trust required |
|---|---|---|---|
| **decode** | bytes → structure | bounded, provable | none |
| **interpret** | structure → meaning under a named machine | possibly unbounded | host opts in and selects the machine |
| **run** | meaning → effects on the world | dangerous | host grants specific capabilities |

Only the first is implicit. That single split provides full expressiveness with none of
the deserialisation CVE class.

### Immediate consequences

- No parse-time includes or imports.
- No expansion primitives that can blow up exponentially.
- No type-name → class resolution.
- No network or filesystem access during decode.
- External references are represented but never followed by the parser.

## Three altitudes of describing behaviour

All three should be representable, and ideally *linked*.

**L0 — opaque artefact plus machine id.** A WASM module, a JAR, a shader, tagged with
which interpreter it needs. Maximally universal, minimally analysable. Hashable and
runnable; not diffable or answerable.

**L1 — structured term.** The behaviour expressed as a tree *in the kernel* — an AST,
not a blob. Inspectable, diffable, rewritable, partially evaluable, searchable. This is
where a universal format earns its keep over "just embed a binary."

**L2 — denotational.** Describe the *result*, not the steps: equations, constraints,
types, a Nix-style derivation, a Datalog rule set. The machine chooses the how.
Strictly more portable, because no execution strategy is baked in.

The valuable design move is letting all three coexist and linking them by provenance —
an L2 specification, an L1 term compiled from it, an L0 artefact compiled from that.
A reader consumes whichever altitude it can handle.

The [Arabic case study](09-case-study-arabic.md) shows this arriving naturally rather
than being contrived: a morphological template *is* a formula from root to surface
form, and `surface = apply(template, root)` is an L2 invariant that a checker verifies
without executing anything at decode time.

## Effects belong in the type

A behaviour value declares what it needs — filesystem, network, clock, randomness,
entropy, unbounded memory — as **structure, before anything runs**. A host can then
refuse in advance rather than discover mid-execution.

Prior art pointing the same way: Unison's ability system, WASM's explicit imports,
capability-based security generally.

"Pure and total" should be a checkable annotation, because a pure formula's hash is a
valid cache key for its result. That composes directly with content addressing:
memoisation, distributed caching, and reproducible builds all fall out.

## The grounding problem

"Given the right machine" recurses. The machine is itself describable as a formula,
which needs a machine, and so on. Two honest resolutions, both of which should be
supported:

**1. A designated floor.** A small set of primitive machines assumed to exist,
identified by hash, with everything else bootstrapped from them. Nock does this in
about twelve opcodes; Guix's full-source bootstrap does it for an entire distribution.
The floor is the trusted computing base, and it should be tiny for the Thompson
"Trusting Trust" reason.

**2. Self-carrying documents.** A document may include, or hash-reference, the
interpreter it requires, terminating at the floor. This is the closest thing to a
genuinely self-contained "anything" — the message brings its own meaning with it.

## Totality and the price paid

Admitting Turing-complete behaviour values means "what does this document mean?" is
undecidable in general. Accept it and quarantine it:

- **Structure stays decidable.** Parsing, hashing, diffing, and schema validation are
  always total.
- **Interpretation may not be.** Anything unbounded runs under an explicit resource
  budget — fuel, gas, step limits — chosen by the host.

## Definitions must stay declarative

A constraint that carries forward into [06](06-composability.md): extension
*definitions* describe structure, canonical form, rendering, and ordering. They are not
arbitrary code. The moment a definition can execute at decode time, the pickle
vulnerability is reintroduced through the extension mechanism.

Anything genuinely computational belongs at the *interpret* step, invoked explicitly,
under fuel.

## Prior art worth reading

- **Unison** — definitions identified by the hash of their normalised AST; code as
  content-addressed data; an effect ("ability") system.
- **Nix** — derivations as declarative formulae for a result rather than scripts;
  content-addressed build outputs.
- **Dhall** — deliberately not Turing-complete, so evaluation always terminates;
  semantic hashing of expressions.
- **WASM + OCI** — a portable, sandboxed machine with explicit imports, distributed by
  content address.
- **OpenMath / MathML** — representing formulae with zero commitment to evaluating them.
- **CUE** — constraints as values.

## The stated non-goal, precisely

> unimsg represents behaviour as inert, inspectable structure, tagged with the machine
> that gives it meaning and the effects it requires. It never executes anything as a
> consequence of being read.

This is not a limitation on expressiveness. It is the precondition for being safe
enough to adopt.