docs: let is lexical-only (always pure); set is the sole mutable-engine write path

AGENTS.md

@@ -22,10 +22,10 @@ Logo dialect.
 
 Anything not on this list is aspirational. Do not assume LANGUAGE.md examples run.
 
-- **Lexer** (`crates/iklo-lexer`) — logos-based; produces `Lexeme` values (kebab-case identifiers, numbers, `:name` lexical refs, `+ - * /` operators, parens, `let`, `be`, `set`, newline, `;`).
+- **Lexer** (`crates/iklo-lexer`) — logos-based; produces `Lexeme` values (kebab-case identifiers, numbers, `:name` lexical refs, `+ - * /` operators, parens, `let`, `be`, newline, `;`). No `set` token exists yet — see Parser/AST below.
 - **AST** (`crates/iklo-ast`) — `Program = Vec<Spanned<Expr>>`; expressions include `Number`, `LexRef`, `Let`, `Binary`.
 - **Parser** (`crates/iklo-parser`) — Pratt precedence; whitespace-sensitive infix ops (so `x-1` stays one identifier); newline is a soft terminator (terminates only when the current expression is complete and can't be continued); `;` is a hard terminator; newlines are swallowed inside parens. Supports `let :name be <expr>` as an expression.
-- **Runtime** (`crates/iklo-runtime`) — tree-walking interpreter with a transactional live image: `RuntimeImage` is a thin façade over `InMemorySubstrate<Value>` (from `iklo-substrate`); `let` and `set` update the image transactionally per top-level expression.
+- **Runtime** (`crates/iklo-runtime`) — tree-walking interpreter with a transactional live image: `RuntimeImage` is a thin façade over `InMemorySubstrate<Value>` (from `iklo-substrate`); `let` updates the image transactionally per top-level expression. `set` is not implemented (no parser/AST support — see above), so it does not update anything today.
 - **Substrate** (`crates/iklo-substrate`) — capability boundary trait (`Substrate` + `Transaction`) that hides where the live image lives. Ships with an in-memory implementation (`InMemorySubstrate`), the default.
 - **Substrate (Turso-backed)** (`crates/iklo-substrate-turso`) — `TursoSubstrate<V>` implementation of `Substrate`, opt-in behind the `turso` Cargo feature (epic [004-turso-substrate-backend](specs/004-turso-substrate-backend/spec.md)); passes the same contract suite as `InMemorySubstrate`. **Local-file-only**: no remote/cloud Turso connectivity (blocker `B001` in that epic's `tasks.md` — a deliberate scoping decision, not a limitation to work around).
 - **CLI** (`crates/iklo-cli`) — file runner and multi-line REPL. Continuation prompt is `iklo. `; blank line cancels a multi-line input. REPL commands are `/`-prefixed (`/quit`, `/revision`, `/env`), recognized only at a fresh prompt, with tab-completion (per ADR-0004). Also selects the substrate backend — see "Substrate mode selection" below.
@@ -35,8 +35,8 @@ Anything not on this list is aspirational. Do not assume LANGUAGE.md examples ru
 These are decided and shouldn't be casually revisited. If a change is needed, open an ADR.
 
 - **Identifiers are kebab-case**, including subtraction-lookalikes: `x-1` is one identifier, `x - 1` is subtraction. Infix `+ - * /` **require whitespace on both sides**.
-- **Binding introduction is `let :name be <expr>`** (not `=`). `:name` is the lexical-value sigil. `let` is an expression that returns the bound value.
-- **`set` mutates an existing binding**; `let` introduces a new one (even if it shadows a previous name). `set` should only reach the mutable engines (graph / dynamic / reactive / synchronized); `set` on a plain lexical binding is an error.
+- **`let :name be <expr>`** (not `=`) introduces a **lexical** binding — the only engine `let` can target. `:name` is the lexical-value sigil. `let` is an expression that returns the bound value, and is always pure (given a pure `<expr>`): lexical bindings are private to the evaluation's own scope and can never be mutated.
+- **`set` is the sole write path for the mutable engines** (graph / dynamic / reactive / synchronized): it creates the binding if absent or mutates it if present (upsert), always effectful either way. `set` on a lexical binding is an error; `let` on a mutable engine is a syntax error — the two verbs partition the engines completely, with no overlap (ADR-0007).
 - **Newline is a soft terminator**: it ends the current expression only when that expression is already complete *and* the next line can't continue it. Newlines are ignored inside `( … )`.
 - **`;` is a hard terminator** and forces the current expression to end (parse error if incomplete).
 - **REPL commands use a leading `/`** (`/quit`, `/revision`, `/env`) recognized only at a fresh prompt; tab-completion is backed by a shared gate function (per ADR-0004). `/` mid-line is division, not a command.

LANGUAGE.md

@@ -210,27 +210,30 @@ let (^bool :y) be -false
 #
 
 # Note: **Everything is a value**
-#       So there's no separate token for type assignment (type declaration + definition).
-#       Meaning `let` can *always* be used to bind an expression <expr> to a token.
-#       Regardless if <expr> is a regular value, a function, a type, or something else entirely...
+#       So there's no separate token for type assignment (type declaration + definition) --
+#       but a bare `^token` (no `:name`) IS a graph binding (the `gra%token`/`^token`
+#       sugar), so per ADR-0007 it goes through `set`, not `let`: type/interface/
+#       computation definitions are new graph bindings, and `set` upserts them.
+#       A "typed val assignment" (`^Type :name be <expr>`, below) stays lexical --
+#       there `^Type` is a type *annotation* on a `let`, not a graph binding.
 
 # simple enum types - similar to sets
-let ^bool be %d{ -true, -false }
+set ^bool to %d{ -true, -false }
 
 # equivalent values, with different type-checking behavior:
 let :x be -true       # a "free" -true should always be parsed as boolean?
 let ^bool :x be -true
 let :x be ^bool -true
 
 # record-like enum types - similar to maps
-let ^maybe be d%{ -left = :value, -right = :value }
+set ^maybe to d%{ -left = :value, -right = :value }
 
 # default construction happens by applying bound type as a function:
 let :val be (^maybe "value1")
 let (^maybe :val) be ^maybe "value2"
 
 # simple record types use slots, not options
-let ^my-record be d%{ :field1 = :value, :field2 = :value, :field3 = d% { -true, -false, -unknown = :unknown-value } }
+set ^my-record to d%{ :field1 = :value, :field2 = :value, :field3 = d% { -true, -false, -unknown = :unknown-value } }
 
 # describe returns generated constructor + field metadata
 let (^my-record :my-record) be ^my-record "my-value" "my-unknown-value"
@@ -239,7 +242,8 @@ let :my-record be ^my-record :value = "my-value", :unknown-value = "my-unknown-v
 # named arguments are valid for any form that declares named slots in its interface
 
 # graph transaction semantics:
-# 1) top-level `let` on graph bindings runs in an implicit transaction
+# 1) top-level `set` on graph bindings (create or update — set is an
+#    upsert, ADR-0007) runs in an implicit transaction
 # 2) nested graph updates require explicit `graph.begin` ... `graph.commit`
 # 3) on uncaught error, graph transaction always rolls back
 # 4) macros can emit graph transactions, but cannot commit a transaction they did not open
@@ -408,7 +412,7 @@ form [:a :b, :n]    # (form [[:a :b], :n])
 | `if%token`   |          | graph        | **Interface binding**: describes the *signature* or *interface* for the *form* and *computation* bindings.                                                                                   |
 | `cp%token`   |          | graph        | **Computation binding**: describes the *compute*/*body* for *form* and *interface* bindings.                                                                                                 |
 | `key%token`  | `~token` | static       | **Keyword** or **Option binding**: *self-bound*, *global*, and *static*. **Cannot be rebound**.                                                                                              |
-| `val%token`  | `:token` | lexical      | **Lexical binding**: *Usually immutable* in iklo. Used for *locals*, *function arguments*, etc.                                                                                              |
+| `val%token`  | `:token` | lexical      | **Lexical binding**: *Immutable once bound* (ADR-0007) in iklo. Used for *locals*, *function arguments*, etc.                                                                                |
 | `var%token`  | `$token` | dynamic      | **Variable binding**: *thread-local* identities with a *shared default*. Like clojure **vars**.                                                                                              |
 | `rx%token`   |          | reactive     | **Reactive binding**: *event-sourced*, *reactive* binding. Like Clojure **agents**.                                                                                                          |
 | `sync%token` |          | synchronised | **Entity binding**: *synchronous* and *uncoordinated*. Like Clojure **atoms**.                                                                                                               |
@@ -424,15 +428,17 @@ form [:a :b, :n]    # (form [[:a :b], :n])
     - **Synchronous** or **Asynchronous**.
     - **Coordinated** or **Uncoordinated**.
 - `graph`, `dynamic`, `reactive` and `synchronized` are always mutable, by definition.
-- `lexical` values are *usually* constant, but can be declared mutable with `set`.
+- `lexical` values are immutable once bound — `let` alone introduces them; `set` never targets the lexical engine (ADR-0007).
 
 
 
 ## Assignment
 
 ```iklo
-# assign an expression to some binding
-let <bound-token> be <expression>    
+# introduce a lexical binding (the only engine `let` can target, ADR-0007)
+let <bound-token> be <expression>
+# write a mutable-engine binding -- create or update, always effectful
+set <bound-token> to <expression>
 ```
 
 
@@ -581,11 +587,18 @@ This is how tokens "interpret themselves" without ambiguous free-form parsing.
       print $a $b
 
       # prints "500 6"
-      let $a be 500 [
+      set $a to 500
+      [
           print $a $b
       ]
-
-      # prints "5 6"
+
+      # TBI/BET: this block illustrated scoped shadow-then-restore for a
+      # dynamic binding (originally written `let $a be 500 [...]`). Per
+      # ADR-0007, `set` is a flat, permanent upsert with no restore-on-exit
+      # of its own -- whether/how a scoped dynamic rebind exists at all
+      # (and what its keyword would be, if not `set`) is unresolved; do not
+      # assume the "prints 5 6" comment below still holds under plain `set`.
+      # prints "5 6" -- UNVERIFIED under the current let/set model, see above
       print $a $b
 
       ### Lexical
@@ -601,8 +614,10 @@ This is how tokens "interpret themselves" without ambiguous free-form parsing.
   ```Iklo
   to some-proc :a :b do
       # Note `some-lambda` has no prefix - this is the "form" binding
-      # Same as `let some-lambda [fn :x :y [return :x + :y]]`:
-      let some-lambda do
+      # (fm%token, graph engine per the Bindings table) -- per ADR-0007,
+      # a new graph binding is introduced via `set`, not `let`.
+      # Same as `set some-lambda to [fn :x :y [return :x + :y]]`:
+      set some-lambda do
           fn :x :y do
               return :x + :y
           end

specs/006-strictness-effects-spike/design-note.md

@@ -24,8 +24,7 @@
 
 | Construct | Strictness | Purity | Effect | Notes |
 |-----------|-----------|--------|--------|-------|
-| Lexical `let :x be <expr>` | strict | pure (binding) | none | Evaluates `<expr>`, binds result in the lexical engine. Transactional commit on success. A `let` targeting a mutable engine (e.g. graph `let ^bool :x be …`, §6) commits engine state and is effectful — the pure row is the lexical form only. |
-| `set :x to <expr>` | strict | effectful (mutation) | mutates existing binding | Requires mutable binding engine (`graph`, `dynamic`, `reactive`, `sync`). |
+| `let :x be <expr>` | strict | pure (binding) | none | Evaluates `<expr>`, binds result. Per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `let` targets the lexical engine only — no engine-level commit to account for, so it is unconditionally pure (given a pure `<expr>`), with no other engine to hedge on. |
 | `+ - * /` (arithmetic) | strict | pure | none | All operands evaluated before computation. |
 | `:x` (lexical read) | strict | pure | none | Returns bound value. |
 | Newline | strict | pure | none | Soft expression terminator; no side effects. |
@@ -35,6 +34,7 @@
 
 | Construct | Strictness | Purity | Effect | Notes |
 |-----------|-----------|--------|--------|-------|
+| `set $x to <expr>` | strict | effectful (mutation) | creates or mutates a mutable-engine binding (upsert) | Not implemented — the parser (`crates/iklo-parser/grammar.lalrpop`) has no `set` production and `iklo-ast::Expr` has no `Set` variant today. The sole write path for mutable binding engines (`graph`, `dynamic`, `reactive`, `synchronized`) once implemented — per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md); never targets `:x` (lexical). |
 | `fn` / `to` (function def) | — | pure (definition) | none | Closure captures lexical env. Body is lazy-evaluated on call. |
 | `cond` | strict branches | pure (control flow) | none | Each branch is strict; only taken branch is evaluated. |
 | `repeat` | strict body | pure (control flow) | none | Body evaluated N times. |
@@ -171,7 +171,7 @@ Runtime metadata (annotations) should **not** be the primary way to declare puri
 The recommended approach:
 
 1. **Surface keywords** (`lazy`, `strict`, `run`, `do`) control the most common cases.
-2. **Type inference** determines purity from the inferred body alone: no observable mutation (e.g. `set` or a graph `let`) and no boundary-crossing during evaluation (no inline `run`/`do`/`then`/boundary `;`). The produced value's type is not itself a purity condition — building an `^action ^t` and returning it is pure; only running it later is effectful (see [ADR-0006](../decisions/ADR-0006-effect-model.md), which is authoritative on this rule).
+2. **Type inference** determines purity from the inferred body alone: no observable mutation (i.e. no `set` — per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `let` can only target the lexical engine, so it never needs naming here) and no boundary-crossing during evaluation (no inline `run`/`do`/`then`/boundary `;`). The produced value's type is not itself a purity condition — building an `^action ^t` and returning it is pure; only running it later is effectful (see [ADR-0006](../decisions/ADR-0006-effect-model.md), which is authoritative on this rule).
 3. **Runtime enforcement** ensures effects only run in effect boundaries.
 4. **Annotations** provide optional hints for tooling and diagnostics.
 
@@ -182,7 +182,7 @@ This avoids the "annotation pollution" problem while keeping effects visible and
 | Example | Strictness | Purity | Effect | Correct? |
 |---------|-----------|--------|--------|----------|
 | `let :x be 1 + 2` | strict | pure | none | Yes — arithmetic is pure and strict. |
-| `set :x to 5` | strict | effectful (mutation) | binding mutation | Yes — rebinds an existing `:x` in a mutable engine; effectful despite returning no `^action` (see §5 point 2). |
+| `set $x to 5` | strict | effectful (mutation) | binding mutation | Yes — upserts `$x` in the dynamic engine (per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `set` never targets lexical `:x`); effectful despite returning no `^action` (see §5 point 2). |
 | `let :x be lazy 1 + 2` | lazy | pure | none | Yes — thunk created, not evaluated. |
 | `strict :x` | strict (force) | pure | none | Yes — forces thunk, may error on cycle. |
 | `let :copy be cp "a" "b"` | strict | pure (builds action) | none (action not run) | Yes — action value created, not executed. |
@@ -192,7 +192,7 @@ This avoids the "annotation pollution" problem while keeping effects visible and
 | `cond (-true) 1 else 2` | strict (branch) | pure | none | Yes — only taken branch evaluated. |
 | `repeat 4 [forward :side]` | strict (body) | pure | none | Yes — body evaluated 4 times, pure. |
 | `to adder :n do fn do :n + 1 end end` | — | pure (definition) | none | Yes — defines closure, no side effects. |
-| Graph `let ^bool :x be -true` | strict | effectful (mutation) | graph commit | Yes — modifies graph binding engine. |
+| Graph `set ^bool to -true` | strict | effectful (mutation) | graph commit | Yes — `set` upserts the graph binding engine; per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `let` can no longer target `graph` at all. |
 | `(vim start)` (shell) | strict | pure (builds action) | process IO only when the action reaches an effect boundary | Yes — builds an `^action ^t`, runs at the same boundaries as any action (top-level runner, `do`, …), per [ADR-0008](../decisions/ADR-0008-shell-executable-calls.md). |
 | `` `[ a ~:b _:c d ] `` (syntax-quote) | — | pure (compile-time) | none | Yes — macro template, no runtime effect. |
 | `map %{ a->1, b->2 }` | strict | pure | none | Yes — literal constructor, pure per contract. |

specs/decisions/ADR-0006-effect-model.md

@@ -64,12 +64,14 @@ their own ADRs (see Follow-ups). They are **not** decided here.
 
 - **Purity is inferred, never declared, and is about evaluation, not the
   produced value's type.** A form is pure iff *evaluating it* performs no
-  observable mutation (no `set`, no `let` into a mutable binding engine —
-  pending ADR-0007's exact line on `set`) and does not itself cross an
-  effect boundary (no inline `run`/`do`/boundary `;`/`then` fires during its
-  own evaluation). Whether the *value* a pure form returns happens to be
-  `^action ^t`-typed is irrelevant — that only means running it *later* is
-  effectful, not that constructing it now was. `let :copy be cp "a" "b"`
+  observable mutation (no `set` — per ADR-0007, `set` is the sole write
+  path for the mutable engines, and `let` can only ever target the lexical
+  engine, so `let` never needs to be named in this exclusion) and does not
+  itself cross an effect boundary (no inline `run`/`do`/boundary `;`/`then`
+  fires during its own evaluation). Whether the *value* a pure form
+  returns happens to be `^action ^t`-typed is irrelevant — that only
+  means running it *later* is effectful, not that constructing it now
+  was. `let :copy be cp "a" "b"`
   above is pure by this rule: it builds an `^action ^int` but never runs
   one. A form that mutates a binding is impure regardless of what it
   returns — that is the failure mode a return-type-only rule would miss
@@ -107,9 +109,11 @@ their own ADRs (see Follow-ups). They are **not** decided here.
   question: forcing a thunk is not on the effect-boundary list in §4 below,
   and `LANGUAGE.md` requires that forcing "must not execute hidden effects"
   — so a thunk body that would mutate a binding or cross a boundary (`set`,
-  a mutable-engine `let`, `run`, `do`, `then`) is **rejected**, not silently
-  deferred. `lazy (set :x to 5)` is ill-typed, exactly like calling `set`
-  directly in any other position where a pure expression is required —
+  `run`, `do`, `then`) is **rejected**, not silently deferred. `lazy (set $x
+  to 5)` is ill-typed, exactly like calling `set` directly in any other
+  position where a pure expression is required — note `:x` (the lexical
+  sigil) could never appear here at all: per ADR-0007, `set` never targets
+  the lexical engine, so `$x` (dynamic) stands in as the example instead —
   laziness does not launder an effect into a runtime action. Laziness is a
   control feature for pure compute, never an effect scheduler
   (`LANGUAGE.md` §"Design constraints"). Forcing a *value's* effect-typed
@@ -148,8 +152,11 @@ semantics":
 
 `run` is the primitive executor; `do` and `then` are effect boundaries in
 their own right that build on it. Nothing else — ordinary expression
-evaluation, thunk forcing, macro expansion, `let`/`set` into a lexical
-binding — is an effect boundary.
+evaluation, thunk forcing, macro expansion, a lexical `let`, or `set` — is
+an effect boundary. `set` (per ADR-0007) is effectful, but it mutates
+*immediately during ordinary evaluation*, gated by the transaction
+contract, not by crossing one of the boundaries above — it is always
+effectful without ever needing one.
 
 ## Non-decisions