From 9973546e3b57c306362ee2d14ae46450003813b9 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 15 May 2026 12:53:20 +0200 Subject: [PATCH] design: feature-acceptance criterion clause 3 + iteration-discipline roadmap milestone MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sharpen the feature-acceptance criterion (DESIGN.md, mirrored in the brainstorm gate) with a third conjunctive-necessary clause: a feature reintroduces no bug class the core constraint exists to eliminate. Criterion 1 ("an LLM reaches for it") does not discriminate — an LLM reaches for every construct native to its imperative training distribution, so utility alone would launder the imperative paradigm back in one construct at a time. Clause 3 is the discriminator; a documentation note is not a reshape (the gate is whether the wrong code fails to typecheck). Record the decided iteration story as a P1 milestone: structural recursion permitted (total-by-construction under Decision 10's acyclic-ADT invariant) + named loop/recur as the only other repetition + tail-app retired. Discharges fieldtest finding F1 without introducing an imperative construct; closes the residual "forgot to mark tail" trap completely; unifies with Decision 10 (acyclic values AND acyclic implicit call graph). Supersedes the "while-loops legal" scope bullet of the Stateful-islands milestone, which is amended for internal consistency. The escaping-state path (ref/MutArray/Stateful) is unaffected and stays in Stateful-islands. --- docs/DESIGN.md | 31 +++++++++++++-- docs/roadmap.md | 77 +++++++++++++++++++++++++++++++++++++- skills/brainstorm/SKILL.md | 17 +++++++-- 3 files changed, 116 insertions(+), 9 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index ded6891..5ca540a 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -70,7 +70,7 @@ is the default. ## Feature-acceptance criterion -A proposed feature ships only if both hold: +A proposed feature ships only if all three hold: 1. **An LLM author naturally produces code that uses it.** Without prompting toward the feature, the LLM reaches for it as the clean @@ -86,10 +86,35 @@ A proposed feature ships only if both hold: edits. Aesthetic appeal — "feels elegant", "is idiomatic" — does not count. +3. **The feature reintroduces no bug class the core constraint exists + to eliminate.** Criterion 1 is necessary but does *not* + discriminate: an LLM reaches for *every* construct native to its + imperative training distribution, so "the LLM reaches for it" is + satisfied by exactly the constructs AILang most deliberately + refuses. A feature can pass 1 and 2 — LLMs reach for it unprompted, + and it removes redundancy — and still be a regression, because it + reinstates the error surface the pure core, local-reasoning, and + RC-acyclicity guarantees were built to remove. The decisive + question is whether the construct re-opens a class of mistakes + (iterated-mutable-state reasoning, silently-unbounded recursion, + reference cycles) that a foundational invariant closes. If it does, + it is cut even when 1 and 2 hold — *or* it must be reshaped until + the bug class is structurally impossible rather than merely + discouraged. A documentation note is not a reshape; the + discriminator is whether the wrong code fails to typecheck, not + whether a guideline advises against it. The canonical worked + example is the iteration story: a bare `while` over mutable state + passes 1 and 2 yet fails 3 (it reinstates iterated-mutable-state + reasoning); structural recursion over an acyclic ADT and a named + loop/recur point pass all three (the bug class is closed by + construction, not by advice). + This is the positive complement to the CLAUDE.md rule that implementation effort is not a rationale: cost is not a reason *for* a -feature, and neither is human aesthetic preference. The only thing -that is, is LLM-author utility. +feature, and neither is human aesthetic preference. LLM-author utility +(1, 2) is necessary; criterion 3 is the discriminator that keeps +utility from laundering the imperative paradigm back in one construct +at a time. Two corollaries: diff --git a/docs/roadmap.md b/docs/roadmap.md index 096f423..4230b5a 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -40,6 +40,76 @@ clean. Pick the next milestone from P2.)_ ## P1 — Next +- [ ] **\[milestone\]** Iteration discipline — structural recursion + + named `loop`/`recur`; recursion-by-call restricted; `tail-app` + retired. The iteration story of the language, decided in principle + 2026-05-15. Two constructs survive, one is removed: + - **Structural recursion stays — and becomes total-by-construction.** + A recursive call is permitted iff it is structurally guarded: + each recursive call is on a constructor-smaller component of an + algebraic argument. Decision 10 already guarantees ADTs are + acyclic, so a structurally-guarded recursion terminates *by the + invariant the language already holds* — permitting it costs + nothing on the provability pillar and it stays locally checkable. + This is the most LLM-natural correct pattern (tree / AST / JSON / + list `match`-and-recurse, saturated in every FP corpus) and must + not be amputated. + - **All other repetition must go through a named `(loop ...)` head + + `recur`.** `recur` is the single explicit backward jump; it + targets a lexically-enclosing named loop, never an implicit fn + head (Clojure permits the implicit form — AILang does not, for + the same no-outward-inference reason that motivated explicit + `tail-app`). Accumulator loops, counted iteration, streaming, + state machines — none are structurally decreasing, so all are + forced into the explicit named-loop form. + - **`tail-app` is retired.** `Term::App { tail: bool }` and the + `musttail`-lowering surface go away: a call is either structural + recursion (a plain call, checked total) or it is `loop`/`recur` + (the only loop). No marked-tail-call concept survives. + + **Motivation.** Discharges fieldtest finding F1 — the most + consequential mut-local finding: mut-local's own motivation + ("removes friction from accumulators that today need tail-recursive + helpers") was structurally unmet, because without a loop the only + iteration mechanism remained the very tail-rec helper. `loop`/`recur` + closes that honestly without introducing an imperative construct + (it is pure: no mutable loop variable, no effect, composes into pure + contexts freely). It also closes the residual "forgot to mark tail" + trap *completely* — a recursive call that is not structurally + guarded is a compile error that names itself, not a silent + stack-overflow. And it unifies with Decision 10: acyclic values + *and* an acyclic implicit call graph; the only cycles anywhere in a + program are explicit, named, typed `loop` points. Both surviving + constructs pass all three feature-acceptance clauses including the + 2026-05-15 clause 3 (structural recursion and named loop/recur are + LLM-natural *and* their bug class is closed by construction; a bare + `while` is exactly what clause 3 rejects). + + **The open spec question (the real brainstorm work).** Not "whether" + but the precise definition of "structurally smaller" / the + guardedness check. Two hard points: (1) *mutual* structural + recursion (needs a measure / size over the ADT, not just a + one-argument syntactic decrease); (2) the accumulator-carrying + structural walk — `foldl`-shaped, simultaneously structural *and* + tail-shaped — the spec must decide whether it counts as structural + recursion (a plain call) or must be expressed as `loop`/`recur`. + This is the load-bearing spec decision; brainstorm + grounding-check + own it. + + **Relation to Stateful islands.** This entry owns the iteration + story and *supersedes* the "while-loops legal" scope bullet of the + Stateful-islands milestone below. The genuinely-escaping + mutable-state path (`ref a` / `MutArray a` / `Stateful a b` / + `pipe`) is unaffected and stays in Stateful-islands — that is the + deliberately-fenced streaming escape hatch for *escaping* state, + not the default iteration story, and F1 no longer motivates it. + + - context: 2026-05-15 chat — design convergence from the + mut-local fieldtest (F1) through the fenced-`while` / + `!Mut`-visibility dead end to the structural-recursion + + named-loop synthesis. Pending brainstorm produces + `docs/specs/-iteration-discipline.md`. + - [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for malloc-backed, refcounted `Str` values alongside the existing static `@.str_*` globals. Today the `Str` path is static-only @@ -319,8 +389,11 @@ clean. Pick the next milestone from P2.)_ - `!Mut` effect, the first non-IO / non-Diverge effect; forces the effect-handler infrastructure forward. - `mut` block as the syntactic boundary in Form A — outside, - AILang's pure self; inside, `var` / `assign` / mutable arrays / - while-loops legal. + AILang's pure self; inside, `var` / `assign` / mutable arrays + legal. (Iteration is *not* part of this boundary: the "Iteration + discipline" P1 milestone supersedes the earlier "while-loops + legal" scope here — repetition is structural recursion or named + `loop`/`recur`, never a `while` over mutable state.) - `var x = expr` + `assign x expr` AST nodes, legal only inside `mut`. - Mutable array primitive (`MutArray a`, O(1) index/update under diff --git a/skills/brainstorm/SKILL.md b/skills/brainstorm/SKILL.md index 1e80f8d..40853f2 100644 --- a/skills/brainstorm/SKILL.md +++ b/skills/brainstorm/SKILL.md @@ -88,14 +88,23 @@ Wait for user choice before proceeding. ### Step 4 — Apply the feature-acceptance criterion -A feature ships only if: +A feature ships only if all three hold: - An LLM author (= future me) naturally produces code that uses it, AND -- The feature measurably improves correctness or removes redundancy. +- The feature measurably improves correctness or removes redundancy, + AND +- It reintroduces no bug class the core constraint exists to + eliminate. Criterion 1 does not discriminate — an LLM reaches for + *every* construct native to its imperative training distribution, + so "the LLM reaches for it" is satisfied by exactly the constructs + AILang most deliberately refuses. A documentation note is not a + reshape: the gate is whether the wrong code fails to typecheck, not + whether a guideline advises against it. Aesthetic appeal does not count. Human ergonomics do not count. If -the answer to either criterion is "I'm not sure", the feature is -probably not ready. The full criterion lives in `docs/DESIGN.md` +the answer to any of the three is "I'm not sure", the feature is +probably not ready. The full criterion (with the canonical worked +example — the iteration story) lives in `docs/DESIGN.md` ("Feature-acceptance criterion"); this skill is the gate that applies it during spec writing.