Brummel
a179ec30a0
First of three iterations of the standalone loop/recur milestone
(spec 97c1ed1). loop/recur become real parseable / printable /
round-trippable / hash-stable strictly-additive AST nodes across
every no-wildcard exhaustive Term match in all six crates, plus
parse/print, prose arms, DESIGN.md + form_a.md schema blocks,
drift/coverage/hash anchors, and the spec's worked sum_to program
as a green round-trip fixture. NO typecheck semantics and NO real
codegen this iter by design: synth and lower_term are stubbed
CheckError::Internal / CodegenError::Internal exactly as mut.1
(real typecheck = iter 2, real loop-header/phi/back-edge = iter 3).
Two binding Boss design calls recorded in the plan header and the
journal: (1) verify_tail_positions "byte-unchanged" = its tail-app
verification role is unchanged, not its source — it is an
exhaustive no-wildcard match so two descent-only arms are
mandatory; acceptance evidence is the tail-app non-regression test.
(2) codegen is in iter-1 scope as stubs/pass-throughs because the
workspace must compile for cargo test --workspace.
Three plan-pseudo-vs-reality substitutions (serde Type::Con
literal, bare Int -> (con Int), unqualified LoopBinder) and one
recon-undercount integration-test site, all intent-preserving and
journalled. Boss forward-fix folded in: the committed specs
themselves wrote bare Int in the loop-binder snippets (parses as
Type::Var) — corrected the three headline snippets to (con Int) for
doc-honesty (no design/schema change).
cargo test --workspace 600 -> 608 / 0 red (Boss-reran
independently); iter13a + new loop_recur hash pins green.
223 lines
9.7 KiB
Markdown
223 lines
9.7 KiB
Markdown
# LLM-Surface Discipline — Design-Principles Spec
|
|
|
|
**Date:** 2026-05-17
|
|
**Status:** Principles distillation — the meta-principle is ratified
|
|
orchestrator guidance; the candidate decisions in §6 are NOT
|
|
ratified and each still requires the normal `brainstorm` +
|
|
Feature-acceptance gate before it touches `DESIGN.md` or is
|
|
implemented.
|
|
**Authors:** Brummel (orchestrator) + Claude
|
|
|
|
## What this spec is
|
|
|
|
A distillation of one design session that walked from "what are
|
|
effects" down through input, world-passing, statefulness,
|
|
closures, recursion, and content-addressing. It is **not** a
|
|
milestone spec: no feature is being proposed for implementation
|
|
here. It records (a) one meta-principle that recurred five times
|
|
and is now treated as standing orchestrator guidance, (b) a
|
|
separability analysis that re-aims the project's cost/benefit
|
|
scrutiny, and (c) a list of open forks with their epistemic
|
|
status so a later `brainstorm` can pick them up without
|
|
re-deriving the reasoning.
|
|
|
|
## What this spec is NOT
|
|
|
|
It does not ratify `loop`/`recur`, closure-private state, the
|
|
removal of `mut`, `argv`-into-`main`, or any change to the cycle
|
|
/ content-addressing commitments. Those are §6 candidates. It
|
|
does not relitigate Decision 10. It carries no implementation
|
|
plan.
|
|
|
|
## 1. The meta-principle (ratified guidance)
|
|
|
|
> **The LLM author writes intent in a disciplined surface form.
|
|
> The raw, mechanical, invariant-threatening transformation stays
|
|
> in the compiler / IR, where the author never hand-manages it.
|
|
> Exposing the raw mechanism to the author is the consistently
|
|
> wrong move for this audience.**
|
|
|
|
This is the operational reading of DESIGN.md's
|
|
Feature-acceptance criterion and the "machine readability over
|
|
human ergonomics" goal, specialised to control/state/effect
|
|
constructs. It is not "hide complexity"; it is "the author
|
|
asserts *what*, the compiler bears the *mechanical invariant*,
|
|
and a violated invariant surfaces as a compile error rather than
|
|
as a silent deep-input failure."
|
|
|
|
## 2. Evidence — the five instances
|
|
|
|
Each row: the disciplined surface AILang keeps (or should keep)
|
|
vs. the raw mechanism it must NOT push onto the author.
|
|
|
|
1. **Effects.** Surface: an effect label on the signature, the
|
|
checker reconciles it. Raw: the author hand-threads a `World`
|
|
token through every call (world-passing). — World-passing is
|
|
sound under Decision 10's uniqueness machinery, but it
|
|
relocates the bookkeeping onto the author. Effect label kept.
|
|
2. **Stateful closures.** Surface: a closure that simply *is* a
|
|
stateful value, its cell born in its own env. Raw: the author
|
|
manages capture + escape + the `mut`→move transport. Closure-
|
|
private state needs no cycles, no weak refs, no linearity-pass
|
|
extension; it is the simplest of the three options examined.
|
|
3. **Move-capture.** Surface: state declared where it is used.
|
|
Raw: a `move`-list, a linearity-pass scope expansion,
|
|
use-after-move diagnostics, per-var-vs-per-block residence.
|
|
Move-capture exists only to *transport* state from an
|
|
enclosing owner to a closure; if the state has no reason to
|
|
exist anywhere but the closure, the transport problem
|
|
dissolves and so does the machinery.
|
|
4. **Iteration / recursion.** Surface: recursion (LLM-natural for
|
|
structural descent) and a single iteration construct. Raw:
|
|
the author hand-compiles a naturally-recursive algorithm into
|
|
an explicit-stack worklist loop. Stack-safety of non-tail
|
|
recursion is the *compiler's* job (cf. the existing
|
|
`(drop-iterative)` escape hatch for the drop cascade), not an
|
|
author obligation discharged by banning recursion.
|
|
5. **Jump.** Surface: `loop`/`recur` — re-iteration is the only
|
|
thing `recur` can mean, the jump is structural. Raw: either
|
|
the author-asserted `tail` flag on `tail-app` (a forgotten
|
|
flag silently degrades to a stack-growing call: correct on
|
|
small inputs, overflow on deep ones — a hallucination-shaped
|
|
failure), or a raw labeled `goto` (kills local reasoning,
|
|
forces mutable loop state, breaks the expression model and
|
|
the structured-AST hash).
|
|
|
|
Five-for-five, the right answer was "disciplined surface,
|
|
mechanism stays in the compiler." This is the through-line.
|
|
|
|
## 3. The robustness corollary
|
|
|
|
For this audience an invariant guaranteed **by construction /
|
|
structurally** strictly dominates one **asserted by the author
|
|
via a flag or annotation**. Rationale: the failure mode of a
|
|
forgotten assertion is silent, input-size-dependent, and
|
|
indistinguishable from correct code in a small test — exactly
|
|
the hallucination-shaped failure the language exists to prevent.
|
|
Canonical anti-example: the `tail-app` `tail: true` flag.
|
|
Canonical positive: `recur`, which has no non-tail spelling.
|
|
|
|
## 4. The separability analysis (re-aims cost scrutiny)
|
|
|
|
`DESIGN.md` bundles three logically distinct commitments as if
|
|
they were one. They are separable:
|
|
|
|
1. **Content-address definitions.** Needs only a canonical
|
|
serialisation + a hash of a finite definition AST. Cheap.
|
|
Delivers the audience-specific wins (verify a symbol without
|
|
spending context; semantic def-diff; trust a signature
|
|
without transitive reading). **Worth it. Keep.**
|
|
2. **Total equational purity of every runtime value.** The
|
|
commitment that forbids the LLM-natural stateful closure.
|
|
Expensive.
|
|
3. **RC without a cycle collector.** Requires acyclic runtime
|
|
values. Expensive.
|
|
|
|
The cost this session repeatedly hit belongs to (2)+(3), not to
|
|
(1). AILang already content-addresses only structure /
|
|
definitions, never live runtime values, so (1) does not require
|
|
the no-cycle memory model — (2) and (3) do. The productive
|
|
question for any future brainstorm is therefore **not** "is
|
|
content-addressing worth it" (it is, and it is cheap) but
|
|
"must value-purity be *total*, or does the weaker line
|
|
**acyclic + unaliased** suffice?" Closure-private state sits
|
|
exactly on that weaker line: not equationally pure, but acyclic
|
|
and unaliased — it keeps (1) and (3) intact while unblocking the
|
|
construct the LLM reaches for.
|
|
|
|
## 5. Concrete surface anchors
|
|
|
|
These pin the *shape* the principles imply. They are
|
|
illustrative, not ratified syntax.
|
|
|
|
Single iteration construct (`loop`/`recur` as pure tail-recursion
|
|
sugar; loop state is rebound parameters, not mutation):
|
|
|
|
```
|
|
(fn sum_to
|
|
(type (fn-type (params (con Int)) (ret (con Int))))
|
|
(params n)
|
|
(body
|
|
(loop (acc (con Int) 0) (i (con Int) 1)
|
|
(if (app > i n)
|
|
acc
|
|
(recur (app + acc i) (app + i 1))))))
|
|
```
|
|
|
|
Closure-private state (state born in the closure; no enclosing
|
|
`mut`, no `move`, no transport):
|
|
|
|
```
|
|
(fn make_counter
|
|
(type (fn-type (params) (ret (fn-type (params) (ret (con Int))))))
|
|
(params)
|
|
(body
|
|
(lam (state (var counter Int 0)) (params) (ret (con Int))
|
|
(body (seq (assign counter (app + counter 1)) counter)))))
|
|
```
|
|
|
|
Cheapest usefulness move (`argv` into `main`; `main(args)` stays
|
|
pure, the impurity stays at the trampoline C-ABI seam — no
|
|
effect, no Decision touched):
|
|
|
|
```
|
|
(fn main
|
|
(type (fn-type (params (con List (con Str))) (ret (con Int))))
|
|
(params args)
|
|
(body ...))
|
|
```
|
|
|
|
## 6. Open forks — candidate decisions, NOT ratified
|
|
|
|
Each needs `brainstorm` + the Feature-acceptance gate before it
|
|
becomes DESIGN.md or a plan. Priority order reflects usefulness
|
|
per cost.
|
|
|
|
1. **`argv` into `main` (highest usefulness per cost).** Moves
|
|
the language out of the closed-program vacuum. Touches no
|
|
Decision; `main(args)` is a pure function, impurity confined
|
|
to the trampoline. One real implementation cost: the
|
|
trampoline must build an RC-correct `List<Str>` (Str slabs +
|
|
cons cells with valid refcount headers) — the in-the-small
|
|
form of the marshalling-into-RC-heap problem. Bounded, local,
|
|
no language-semantics change.
|
|
2. **`loop`/`recur` as the single iteration surface.** Re-attempt
|
|
of the reverted Iteration-discipline centrepiece, but
|
|
**standalone** — de-bundled from the structural-guardedness
|
|
checker and the `Diverge` effect that entangled and sank the
|
|
original milestone. Honest cost to spec explicitly: retiring
|
|
`tail-app` wholesale loses general proper-tail-calls (mutual
|
|
recursion, tail-call into a different fn) with a stack
|
|
guarantee. State the cost in the spec; do not retire it
|
|
silently.
|
|
3. **Closure-private mutable state, possibly replacing `mut`.**
|
|
Sealed scalar `mut` without loop and without capture is
|
|
largely redundant with `let`/`if`/`match`; its only on-record
|
|
justification is the narrow ergonomic mut-local fieldtest
|
|
finding. Removing a shipped, fieldtested feature requires the
|
|
project's own empirical gate: re-author the mut-local
|
|
fieldtest tasks with closure-private state + plain `let`; if
|
|
the reported hallucination friction does not return, `mut` is
|
|
scaffolding and can fall, and the move-capture milestone is
|
|
then unnecessary (it solved a transport problem that only
|
|
existed because `mut` births state in the wrong place).
|
|
4. **Cycles / content-addressing (deepest; deliberately not
|
|
opened).** Allowing cycles to get "real" closures negates
|
|
Decision 10 and transitively Decision 1/2. Per §4 it is the
|
|
wrong target anyway — the cheap, high-value commitment
|
|
(content-address definitions) is not the expensive one. Named
|
|
here as the deepest fork so it is not stumbled into; a
|
|
near-term milestone must not open it.
|
|
|
|
## Cross-references
|
|
|
|
- `docs/DESIGN.md` — Decision 1/2 (source = data, content-
|
|
addressed), Decision 3 (pure core + effects), Decision 8
|
|
(verified tail calls), Decision 9/10 (RC + uniqueness, no
|
|
collector), Feature-acceptance criterion.
|
|
- `docs/specs/2026-05-15-mut-local.md` — the sealed-mut milestone
|
|
whose redundancy §6.3 questions.
|
|
- `docs/specs/2026-05-16-iteration-discipline-revert.md` — why
|
|
the bundled loop/recur milestone was backed out; §6.2 is the
|
|
de-bundled re-attempt.
|