# Remove `mut` / `var` / `assign` — Design Spec

**Date:** 2026-05-18
**Status:** Draft — awaiting user spec review
**Authors:** Brummel (orchestrator) + Claude

## Goal

Remove the local-mutable-state construct from AILang entirely. At
the AST there are exactly two nodes — `Term::Mut` (the block, which
declares the vars) and `Term::Assign` (the update); `var` is not a
first-class `Term`, only the declaration syntax inside a `mut`
block, and `Term::Assign` is statically illegal outside an enclosing
`Term::Mut` (`mut-assign-out-of-scope`). The three keywords are one
indivisible feature; the cut is atomic.

The feature-acceptance criterion, applied **inverted** (does the
*removed* feature fail the gate?):

- **Clause 1** (an LLM author reaches for it): met — and per
  `docs/DESIGN.md` that counts *against*, not for, since clause 1 is
  satisfied by exactly the imperative constructs the core refuses.
- **Clause 2** (removes redundancy / improves correctness):
  violated. Every one of the shipped `mut`-bearing fixtures is
  straight-line scalar mutation a `let`/`if` expresses; the
  iteration ones delegate to a tail-recursive helper. The construct
  *is* the redundancy. Proven executable below (`mut_counter.ail`
  before→after).
- **Clause 3** (reintroduces no bug class the core exists to
  eliminate): violated. `Term::Mut` + `Term::Assign` is the
  iterated/sequenced mutable-state reasoning `docs/DESIGN.md`
  lines 99–108 name as the canonical clause-3 failure. Scalar
  sealing bounds the blast radius, not the reasoning burden — and
  nothing in-tree needs it.

`loop` / `recur` shipped and closed as a standalone milestone
(2026-05-18) and is the surviving first-class iteration construct;
`let` / `if` cover the straight-line cases. This milestone is
explicitly **decoupled** from the open "Stateful islands" roadmap
item, which is a separate, later, independent decision and is **not**
in scope here.

## Architecture

Atomic hard-removal in one milestone, no deprecation window
(Approach A). Surface, AST, checker, codegen, DESIGN.md, fixtures
and the drift trio are all cut together so the schema is honest at
every commit.

After removal the Form-A keywords `mut` / `var` / `assign` no longer
lex; a JSON-AST carrying `{"t":"mut"}` or `{"t":"assign"}` fails
closed as a generic serde unknown-variant error. There is **no**
dedicated "construct removed" diagnostic — a tombstone diagnostic is
permanent clutter for a language whose sole author is an LLM that
simply stops emitting `mut` once `docs/DESIGN.md` no longer
documents it (no-nostalgia).

One delicate interaction governs the whole milestone: **the codegen
alloca machinery is shared with `loop`.** `loop-recur.3` lowered
loop binders by reusing the mut.3 `pending_entry_allocas` mechanism
and registering them in the existing `mut_var_allocas` map, and
`loop-recur.tidy` widened the shared `Term::Lam` escape guard to
cover both. The machinery therefore **survives** the cut (loop needs
it); only its `mut` half is removed, and the now-misnamed
`mut_var_allocas` is renamed `binder_allocas` for honesty (its
"mut-var" name would otherwise be a lie in the source).

## Concrete code shapes

### The AILang program — inverted clause-1 faithfulness evidence

The headline is the proof that removal loses **no** expressivity:
every shipped `mut` program rewrites to an observably identical
`let`/`if` program. Two real fixtures, before → after:

`examples/mut_counter.ail` (the strongest evidence — the `mut` block
computed *nothing*; the iteration was always the tail-recursive
helper):

```clojure
;; BEFORE — ships today (mut.3 fixture), prints 55
(fn main
  (type (fn-type (params) (ret (con Unit)) (effects IO)))
  (params)
  (body
    (app print
      (mut
        (var sum (con Int) 0)
        (assign sum (app sum_helper 1 10 0))
        sum))))

;; AFTER — observably identical, prints 55
(fn main
  (type (fn-type (params) (ret (con Unit)) (effects IO)))
  (params)
  (body
    (app print (app sum_helper 1 10 0))))
;; sum_helper (tail-recursive accumulator) is unchanged.
```

`examples/mut.ail` :: `mut_single_var` (the minimal scalar case):

```clojure
;; BEFORE — value is 1
(body
  (mut
    (var x (con Int) 0)
    (assign x (app + x 1))
    x))

;; AFTER — value is 1, faithful
(body
  (let x 0 (app + x 1)))
```

`mut.ail` :: `mut_nested_shadow` shows the rewrite also *exposes*
the redundancy — the outer `var`+`assign` was dead code `mut`
permitted (only the inner block is the body's value):

```clojure
;; BEFORE — value 101 (outer x=10,x+1 discarded; inner x=100,x+1 returned)
(body
  (mut (var x (con Int) 10) (assign x (app + x 1))
    (mut (var x (con Int) 100) (assign x (app + x 1)) x)))

;; AFTER — value 101, the dead outer state simply gone
(body
  (let x 100 (app + x 1)))
```

The must-fail side (the removal made executable): a module carrying
`{"t":"mut"}` / a `.ail` with the `mut` keyword must now be
rejected (serde unknown-variant / Form-A parse error). This is a new
pin fixture, the clause-3 discriminator (the wrong code fails to
typecheck, not merely advised against).

### Implementation shape (secondary — supporting, not the point)

| Site | Before | After |
|---|---|---|
| `ailang-core/src/ast.rs` (~529-638) | `Term::Mut { vars: Vec<MutVar>, body }`, `Term::Assign { name, value }`, `struct MutVar { name, ty, init }` | all three deleted; every exhaustive no-`_`-wildcard `Term` match across the 6 crates loses its `Mut`/`Assign` arms |
| `ailang-surface` (`lex`/`parse`/`print`/`loader.rs`, `form_a.md`) | `mut`/`var`/`assign` keywords, `parse_mut`/`parse_assign`, print arms | deleted; the keywords no longer lex |
| `ailang-check/src/lib.rs` | `Term::Mut`/`Term::Assign` synth arms; `mut_scope_stack` threaded through every synth caller; 4 variants `MutVarCapturedByLambda`, `UnsupportedMutVarType`[`mut-var-unsupported-type`], `MutAssignOutOfScope`[`mut-assign-out-of-scope`], `AssignTypeMismatch`[`assign-type-mismatch`] + their `code()`/`ctx()` arms; shared `Term::Lam` escape guard gate `!mut_scope_stack.is_empty() \|\| !loop_stack.is_empty()` | synth arms + `mut_scope_stack` + the 4 variants deleted; escape-guard gate simplifies to `!loop_stack.is_empty()`, the `mut_scope_stack` free-var pass removed — **the `loop_stack` half MUST survive byte-equivalent** (loop-binder-captured-by-lambda still rejected) |
| `ailang-codegen` (`lib.rs` ~1779-1855, `escape.rs` ~193-417, `lambda.rs`) | `Term::Mut`/`Term::Assign` `lower_term` arms; `mut_var_allocas`/`pending_entry_allocas` save/restore | the two `lower_term` arms + the `mut`/`assign` escape arms deleted; the alloca machinery **kept** (loop reuses it) and `mut_var_allocas` renamed `binder_allocas`, doc-comments made truthful |
| `docs/DESIGN.md` | `Term::Mut`/`Term::Assign` data-model entries (~2404-2422) + mut.1/mut.3/mut.4 prose (~2448-2458) + the symmetric lambda-capture note | the `mut` data-model + prose hard-deleted; the symmetric-rule note keeps only its `loop`-binder half; present-tense, zero nostalgia |
| drift trio + `carve_out_inventory.rs` + roadmap | mut anchors in `design_schema_drift`/`spec_drift`/`schema_coverage`; mut carve-out fixtures counted in `EXPECTED` (18 post-loop-recur.tidy); roadmap "mut-local is the foundation for Stateful islands" sub-bullet | mut drift anchors removed in lockstep with the schema deletion; `EXPECTED` decremented by the mut carve-out count (exact integer = planner's to pin); the false foundation sub-bullet removed |

## Components

1. **AST** — delete the two variants and `MutVar`; sweep every
   exhaustive `Term` match (the same ~30-site no-wildcard pattern
   `loop-recur.1` swept additively, now in reverse).
2. **Surface** — delete keyword lexing, the two parsers, the print
   arms, the loader handling, the `form_a.md` grammar lines.
3. **Checker** — delete synth arms, `mut_scope_stack` threading,
   the 4 `CheckError` variants + registry/ctx arms; simplify the
   *shared* escape guard to `loop_stack`-only, preserving the
   loop-binder rejection exactly.
4. **Codegen** — delete the two `lower_term` arms + `escape.rs`/
   `lambda.rs` `mut` handling; **keep** the alloca machinery
   (loop-carried), rename `mut_var_allocas` → `binder_allocas`.
5. **Fixtures** — rewrite value-computing fixtures to `let`/`if`
   (`examples/mut.ail` 6 fns, `mut_counter.ail`, `mut_sum_floats.ail`,
   `fieldtest/mut-local_1..4`), repoint the e2e assertions
   (`mut_counter`→55, `mut_sum_floats`→55); **delete** the
   rejection-probe fixtures whose entire purpose is the removed
   mut-specific rejection (`fieldtest/mut-local_5_lambda_capture_probe.ail`,
   `mut-local_6_diag_probe.ail`, `examples/test_mut_var_captured_by_lambda.ail.json`)
   — no `let`/`if` equivalent exists for them.
6. **DESIGN.md** — hard-delete the `mut` data-model + prose;
   present-tense; the file must read as the *current* language, with
   no trace of `mut`/`var`/`assign` and no post-mortem.
7. **Drift trio + roadmap** — remove mut anchors in lockstep with
   the schema deletion (proves removal is matched by pin removal);
   decrement `carve_out_inventory` `EXPECTED`; delete the false
   Stateful-islands "foundation" sub-bullet.

## Data flow

Author writes `.ail` with `let`/`if`/`loop`/`recur` only → surface
no longer lexes `mut`/`var`/`assign` (Form-A parse error on the
keyword) → JSON-AST has no `"t":"mut"`/`"t":"assign"` (serde
unknown-variant rejection, fail-closed) → checker/codegen never see
the nodes. Non-`mut` modules are byte-stable end-to-end: removal is
symmetric to the additive mut.1 introduction and serde is
tag-based, so no canonical-JSON hash of any surviving module moves.
`loop`/`recur` is unaffected — it shares the renamed alloca
machinery, and its lowering is byte-identical (rename is
representation-only).

## Error handling

The 4 `mut` `CheckError` variants are deleted. `{"t":"mut"}` /
`{"t":"assign"}` produce the generic serde unknown-variant error —
no dedicated diagnostic, no tombstone (fail-closed, no-nostalgia).
`loop`/`recur`'s five `Recur*` codes and `LoopBinderCapturedByLambda`
are byte-unchanged. The shared `Term::Lam` escape guard must keep
rejecting a lambda that captures a `loop` binder — this is a
non-regression pin, since the guard is the exact code being
simplified.

## Testing strategy

- **Behaviour-preservation (inverted clause-1, executable):** the
  rewritten fixtures' e2e value assertions stay green —
  `mut_counter`→`55`, `mut_sum_floats`→`55` — proving the `let`/`if`
  rewrite is faithful.
- **loop/recur non-regression:** the full `loop_recur_*` /
  `loop_sum_to*` fixture suite byte-identical (the shared
  alloca-machinery rename must not move loop codegen); the
  `loop-binder-captured-by-lambda` rejection still fires
  point-exactly (shared escape guard, loop half survives);
  `tail-app`/`tail-do` byte-frozen.
- **Schema honesty:** drift trio (`design_schema_drift`,
  `spec_drift`, `schema_coverage`) + `carve_out_inventory` green at
  the new `EXPECTED` — proving the schema-region deletion is
  matched by the drift-anchor deletion.
- **Removal made executable:** a new must-fail pin — a `.ail` with
  the `mut` keyword and a module with `{"t":"mut"}` are now rejected
  (Form-A parse error / serde unknown-variant).
- **Round-trip invariant:** all surviving non-`mut` modules
  `ail parse|render|parse` byte-identical; pre-existing hash pins
  byte-stable.
- `cargo test --workspace` green.

## Acceptance criteria

- `mut`/`var`/`assign` do not lex in Form A; `{"t":"mut"}` /
  `{"t":"assign"}` are rejected as unknown serde variants; no
  `Term::Mut`/`Term::Assign`/`MutVar` symbol remains in any crate.
- The 4 `mut` `CheckError` variants are gone; `loop`/`recur`'s
  codes and the loop-binder escape-guard behaviour are
  byte-unchanged (non-regression pinned).
- Every value-computing fixture is rewritten faithfully and still
  produces its original value (`mut_counter`/`mut_sum_floats`
  print 55); the three rejection-probe fixtures are deleted.
- `docs/DESIGN.md` is present-tense and contains zero
  `mut`/`var`/`assign` mention and zero nostalgia/aspiration; the
  drift trio + `carve_out_inventory` are green at the new
  `EXPECTED`.
- The Roundtrip Invariant holds byte-identically for all surviving
  modules; the `loop`/`recur` e2e (`55` / `500000500000` /
  infinite-compiles) stay green.
- `cargo test --workspace` green; milestone-close `audit` bench
  baseline pristine (pure removal, no hot-path touched — any
  non-pristine result is a defect, not a ratifiable delta).