diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 5a0ca7c..b95826d 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -113,6 +113,233 @@ Rationale:
 Trade-off: no inline optimisations through the LLVM API. We rely on
 `clang -O2` as the standard pipeline.
 
+## Decision 6: authoring surface (Iter 14b — WIP)
+
+**Status: design pass in progress.** Reading without skipping the JOURNAL
+will leave this section ahead of the implementation.
+
+### Why this is opening up
+
+Iters 1 through 14a authored everything as raw `*.ail.json`. That worked
+for 17 fixture files (each ≤ 60 LOC of JSON) but does not scale. Two
+breaking signals:
+
+1. The token-economy cost of the JSON-AST is massive: a single integer
+   literal `1` is encoded as `{"t":"lit","lit":{"kind":"int","value":1}}`
+   — ~38 tokens of structural overhead per bit of semantics. For a stdlib
+   in the 200–500 def range this displaces real attention budget.
+2. JSON-AST authoring exposes a class of errors (wrong field names,
+   silently-accepted extra fields under `#[serde(default)]`,
+   inconsistent ctor casing) that surface only at load time. The
+   schema is correct-by-construction in storage but **error-prone in
+   authoring**.
+
+Decision 1 anticipated this: it says a textual form exists "as a
+bidirectional projection of the JSON form." The pretty-printer already
+emits S-expression-style text (see `crates/ailang-core/src/pretty.rs`).
+What is missing is the inverse direction — text → AST. Decision 6
+makes that inverse the canonical authoring surface, with JSON-AST
+demoted to "storage and exchange" only.
+
+### Constraints (hard, in priority order)
+
+1. **Formalizable for a foreign LLM.** The grammar must fit in an
+   EBNF/PEG spec of ≤ 30 productions. A model that has never seen
+   AILang must be able to read the spec and produce conforming source
+   zero-shot. Rules out: precedence between binary operators,
+   semantic indentation, maximal-munch lexing, context-sensitive
+   reductions.
+2. **AST-isomorphic.** Every surface form maps to exactly one AST
+   shape. Round-trip surface → AST → canonical JSON → AST → surface
+   is the identity (modulo formatting). Hashes computed via the
+   round-tripped JSON must equal hashes of the same module written
+   directly in JSON.
+3. **No external symbols.** ASCII only. No Greek (`∀`), no arrows
+   (`→`), no subscripts. Reasoning: I substitute mojibake for
+   non-ASCII characters under context pressure; foreign LLMs vary
+   in how they tokenize Unicode.
+4. **No precedence.** Either everything is parenthesized, or there
+   are no infix operators. Prefer the latter — `add(x, 1)` over
+   `x + 1`. Removes a fail mode for both me and foreign LLMs.
+5. **No semantic indentation.** Block structure expressed by paired
+   delimiters or terminator tokens. Indentation is informational
+   only; the parser ignores it.
+6. **One construct per token-list.** Every AST node corresponds to
+   exactly one parenthesized form (or atom). No "sometimes you can
+   omit the parens" rules.
+7. **AST surface stays frozen.** The surface adapts to the AST, not
+   the other way around. We do not change the JSON schema or
+   invalidate hashes to make the surface prettier.
+
+### Candidate notations (same `map` encoded in each)
+
+The reference target — the polymorphic `map` from `examples/list_map_poly.ail.json`:
+
+```
+data List a where Nil | Cons a (List a)
+fn map : forall a b. ((a) -> b, List a) -> List b
+       = \f xs. match xs of Nil -> Nil
+                          | Cons h t -> Cons(f(h), map(f, t))
+```
+
+#### (A) S-expression with fully-tagged AST nodes
+
+```
+(module list_map_poly
+
+  (data List (vars a)
+    (ctor Nil)
+    (ctor Cons a (con List a)))
+
+  (fn inc
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params x)
+    (body (app + x 1)))
+
+  (fn map
+    (type
+      (forall (vars a b)
+        (fn-type
+          (params (fn-type (params a) (ret b)) (con List a))
+          (ret (con List b)))))
+    (params f xs)
+    (body
+      (match xs
+        (case (pat-ctor Nil) (term-ctor List Nil))
+        (case (pat-ctor Cons h t)
+          (term-ctor List Cons
+            (app f h)
+            (app map f t)))))))
+```
+
+Grammar core (3-rule lexical layer + ~25 named-form productions):
+```
+sexpr  ::= atom | "(" sexpr* ")"
+atom   ::= integer | string | ident
+ident  ::= any maximal non-whitespace, non-paren run that is not
+           a recognised integer or string literal.
+```
+
+The lexer recognises one delimiter (`(` / `)`) and whitespace.
+Every other maximal token is classified post-hoc:
+- All-digit run with optional leading `-` → integer atom.
+- `"`-delimited run → string atom.
+- Otherwise → ident.
+
+Consequence: operators like `+`, `==`, `<=`, `**`, qualified
+names like `io/print_int`, and cross-module references like
+`std_list.map` are all single ident tokens with no special lex
+rule. The only reserved tokens are `(`, `)`, and whitespace.
+Bool literals (`true`, `false`) and unit (`(lit-unit)`) are
+disambiguated by parser context, not by lex.
+
+Every AST node form has a unique head keyword (`module`, `data`,
+`fn`, `forall`, `fn-type`, `con`, `var`, `app`, `lam`, `match`,
+`case`, `pat-ctor`, `term-ctor`, `do`, `seq`, ...). A bare atom in
+a positional slot (e.g. inside `(con List a)` second position) is
+a name reference whose **sort** is determined by the parent slot:
+
+- inside `(con NAME args...)` second-and-later positions → type
+  expression. Bare atom there ⇒ `Type::Var { name }`.
+- inside `(app HEAD args...)` first position ⇒ `Term::Var`.
+- inside `(pat-ctor CTOR fields...)` field positions ⇒
+  `Pattern::Var`.
+- inside `(case PAT BODY)` second position ⇒ term.
+
+There is **no lexical case rule**. To construct a value with a
+ctor, write `(term-ctor TypeName CtorName args...)`. To match
+against one, write `(pat-ctor CtorName fields...)`. Capitalised
+identifiers carry no special meaning to the parser. This rules
+out a class of silent errors ("I forgot to capitalise `Cons` and
+it parsed as a function call").
+
+**Pros:** smallest formal grammar of any candidate (the lexical
+core is 3 rules; the named-form productions are uniform — every
+node a tagged list). Foreign-LLM bar lowest. Round-trip with the
+existing pretty-printer is a refactor of `pretty.rs` to emit this
+tagged form, plus a new parser.
+
+**Cons:** paren density is high. `(forall (vars a b) (fn-type
+...))` has more visual nesting than the current pretty-printer's
+`forall a. (...) -> ...`. Verbosity is ~2× JSON for the same node
+when measured in characters, but ~8× shorter in lines (the
+existing JSON `box.ail.json` of 160 lines becomes ~20 lines in
+this form).
+
+#### (B) Indented record-style with explicit terminators
+
+```
+module std_list
+
+data List(a):
+  Nil
+  Cons(a, List(a))
+end
+
+fn map:
+  type: forall a b. fn(fn(a) -> b, List(a)) -> List(b)
+  params: f, xs
+  body:
+    match xs:
+      Nil          => Nil
+      Cons(h, t)   => Cons(f(h), map(f, t))
+    end
+end
+```
+
+Grammar core (~20–30 productions): module-level (def/data/end), type
+sub-grammar (forall, fn, con, var), term sub-grammar (lam, match,
+ctor, app, lit, var, seq), pattern sub-grammar.
+
+**Pros:** higher information density per line, closer to mainstream
+ML/Haskell shape. **Cons:** four sub-grammars instead of one.
+`forall a b. fn(...)` keeps a pseudo-precedence (`->` binds tighter
+than the outer `fn(...)` wrapper). Foreign-LLM bar higher.
+
+#### (C) Pretty-printer-as-source
+
+Use exactly the format `pretty::module` already emits, plus a parser
+that accepts it. The existing pretty-printer's quirks (`::` for
+type-of, `[params]` for fn-params, `<a>` for type-args, `forall a. ...`,
+`!IO`, `()` ambiguous between unit-arg-list and empty-form) become
+the spec.
+
+**Pros:** zero churn — the existing pretty-printer is already the
+spec; only the inverse is missing. Round-trip is the identity by
+construction. **Cons:** the existing format mixes four mini-dialects
+(s-expr at term level, ML-shape at type level, square brackets for
+params, `<>` for type args). Formalising it crisply is harder than
+designing a uniform form from scratch.
+
+### First choice and rollback plan
+
+**Try (A) first.** Reasoning: constraint 1 (formalizable) outweighs
+constraint readability. (A) has a 3-rule core grammar with one
+lexical disambiguation rule. (B) doubles the rule count and
+re-introduces a soft form of precedence (`->` inside `forall`).
+(C) is tempting because it is zero-design but the resulting spec is
+visibly heterogeneous, which is exactly what constraint 1 was meant
+to rule out.
+
+If implementing (A) reveals that paren density actively hurts my
+authoring (measurable: I make more wrong-paren errors than the
+JSON-AST shape produced before), roll back and try (C). (B) stays
+on the shelf for a future iter only if both fail.
+
+### Implementation outline (Iter 14c onwards, not done in 14b)
+
+- `crates/ailang-surface` — new crate. PEG parser → existing
+  `ailang-core::ast` types. No new AST nodes.
+- Round-trip test: every `examples/*.ail.json` → emit via
+  `pretty::module` → parse via new crate → re-canonicalise →
+  hash-equivalent to original. Hash equivalence is the truth check;
+  no surface form ships if a single fixture loses its hash.
+- CLI: `ail parse <surface-file> -o <json-file>`. Symmetric to the
+  existing `ail render`.
+- Then: rewrite one existing fixture (probably `box.ail.json`) in
+  the surface, hash-compare, commit both forms. Stdlib starts in
+  the surface from day one.
+
 ## Mangling scheme (Iter 5c)
 
 All AILang functions are mangled to `@ail_<module>_<def>` — even in the
diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md
index a510dc3..71d408d 100644
--- a/docs/JOURNAL.md
+++ b/docs/JOURNAL.md
@@ -1513,3 +1513,118 @@ itself surface more dogfood bugs. The original 14b
 (GC/arena) and 14c (poly fn as value) remain on the queue
 but have not had a design pass.
 
+## Iter 14b — design pass for the authoring surface
+
+User redirected the project at the iter boundary. I had been
+about to write a stdlib in JSON-AST form; user pushed back: do
+I really program *best* in JSON, given the language is supposed
+to be the one I'm most accurate in? Honest answer was no — JSON
+was rationalisation. The constraint added in this iter:
+
+> "Die Syntax sollte gut formalisierbar sein, damit man auch
+> einem fremden LLM eine Spec geben kann, die es dann fehlerfrei
+> befolgt."
+
+That single sentence ruled out about half the design space:
+anything with operator precedence (precedence is the #1 thing
+an LLM gets wrong when handed a spec, because it requires
+building a parse-tree mental model rather than just following
+production rules), anything with semantic indentation, anything
+with maximal-munch lexing or context-sensitive reductions.
+
+What remains is roughly: S-expressions, or dialects close to
+S-expressions. Decision 6 in DESIGN.md captures the constraints
+in priority order, sketches three candidate forms (A: tagged
+S-expression, B: indented record-style, C: pretty-printer-as-
+source), and picks (A) as the first attempt with explicit
+rollback to (C) if (A) hurts authoring more than it helps.
+
+**Key shape of (A):** every AST node has a unique head keyword.
+No case-disambiguation rule (no "capitalised head means ctor").
+Bare atoms in positional slots get their sort from the parent
+slot (inside `(con NAME args...)` second-and-later positions
+are types; inside `(app HEAD args...)` first position is a term;
+etc.). To construct a value with a ctor, write
+`(term-ctor TypeName CtorName args...)` explicitly. To match,
+`(pat-ctor CtorName fields...)`. The capitalisation/case of an
+identifier carries no semantic weight to the parser.
+
+This rules out the silent-error class "I forgot to capitalise
+`Cons` and it parsed as a function call" — which I had been
+relying on case-conventions to prevent in the JSON form too,
+but only by hand-discipline. With explicit tags the discipline
+becomes a parse rule.
+
+**Empirical test (this iter).** Hand-encoded three examples in
+form (A) as `examples/*.ailx`:
+
+```
+hello.ailx          —   5 LOC (was JSON: 36 pretty / 21 canonical)
+box.ailx            —  25 LOC (was JSON: 160 pretty / 88 canonical)
+list_map_poly.ailx  —  50 LOC (was JSON: 394 pretty / 230 canonical)
+```
+
+Roughly 4–8× line reduction, ~4× character reduction. Bigger
+gains on bigger programs (overhead is proportional to AST
+depth, not to program size, so the form scales well). All three
+mapped unambiguously to AST nodes by inspection — no
+ambiguities surfaced during writing that the spec didn't
+already cover.
+
+Two small lex/grammar issues I discovered while writing and
+folded back into DESIGN.md before committing:
+
+1. **Operator idents** like `+`, `==`, `<=`. Initial spec had a
+   word-shaped `[A-Za-z_]...` regex; that excluded operators.
+   Fix: lexer recognises only `(`/`)`/whitespace as delimiters.
+   Every other maximal token is classified by first character
+   (digit ⇒ integer, `"` ⇒ string, else ⇒ ident). `+`, `42`,
+   `io/print_int`, `==` all become single ident or integer
+   tokens with no special rule.
+2. **Bool literals.** Bare `true`/`false` are reserved in term
+   context; outside term context they would be ill-formed
+   anyway. Unit is explicit: `(lit-unit)`.
+
+**Files touched:**
+- `docs/DESIGN.md` — Decision 6 added (~140 lines), with
+  constraints, three candidates, first-choice rationale, and
+  an implementation outline for Iter 14c.
+- `examples/hello.ailx`, `examples/box.ailx`,
+  `examples/list_map_poly.ailx` — three design exhibits. Not
+  parseable yet (header comment says so).
+- `docs/JOURNAL.md` — this entry.
+
+**Tests:** None new. Existing 25/25 e2e + 3 ignored doctests
+unchanged (this iter is paper, not code). `cargo doc --no-deps`
+0 warnings (workspace invariant from 13d/e/f preserved).
+
+**Process note: orchestration with explicit licence to be
+wrong.** User said "du darfst auch ausprobieren und dich irren
+(und es dann rückgängig machen). Wir wollen das beste Design
+für den propagierten Zweck." That changes the cost model for
+design iteration: I should optimise for *information per iter*,
+not for *correctness on first commit*. So I committed form (A)
+as a working hypothesis with a documented rollback path to
+form (C), rather than design-by-committee until I was sure.
+
+**Plan 14c (next).**
+1. New crate `ailang-surface` with a small PEG parser → existing
+   `ailang-core::ast` types. No new AST nodes.
+2. Round-trip test gate: every existing `examples/*.ail.json`
+   gets a sibling `*.ailx` written by hand or by an
+   AST→surface emitter; the test parses the surface, canonises
+   to JSON, and asserts hash-equivalence to the original. If a
+   single fixture loses its hash, the form does not ship.
+3. CLI: `ail parse <file.ailx> -o <file.ail.json>`. Symmetric
+   to existing `ail render`.
+4. If round-trip works for all current fixtures, mark form (A)
+   confirmed and start the stdlib in `.ailx` directly. If it
+   fails, document why in JOURNAL and try (C).
+
+**Plan 14d (after 14c).** First stdlib module: `std_list.ailx`
+with `length`, `filter`, `fold`, `concat`, `reverse`, `head`,
+`tail`. Each combinator is a fresh test vector for codegen and
+for the still-young parameterised-ADT pipeline. Written in the
+new surface from day one — no JSON authoring of stdlib.
+
+
diff --git a/examples/box.ailx b/examples/box.ailx
new file mode 100644
index 0000000..df1493b
--- /dev/null
+++ b/examples/box.ailx
@@ -0,0 +1,36 @@
+; Iter 14b design exhibit — Decision 6 form (A).
+; This file is NOT yet parseable by `ail`. The parser lands in
+; Iter 14c. Hash-equivalence with `box.ail.json` is the round-trip
+; test that gates that iter.
+
+(module box
+
+  (data Box (vars a)
+    (doc "A unary box around a polymorphic value.")
+    (ctor MkBox a))
+
+  (fn unbox
+    (doc "Polymorphic projection out of a Box.")
+    (type
+      (forall (vars a)
+        (fn-type
+          (params (con Box a))
+          (ret a))))
+    (params b)
+    (body
+      (match b
+        (case (pat-ctor MkBox x)
+          x))))
+
+  (fn main
+    (doc "Round-trip 42 through MkBox + unbox.")
+    (type
+      (fn-type
+        (params)
+        (ret (con Unit))
+        (effects IO)))
+    (params)
+    (body
+      (do io/print_int
+        (app unbox
+          (term-ctor Box MkBox 42))))))
diff --git a/examples/hello.ailx b/examples/hello.ailx
new file mode 100644
index 0000000..425a55c
--- /dev/null
+++ b/examples/hello.ailx
@@ -0,0 +1,8 @@
+; Iter 14b design exhibit — Decision 6 form (A).
+; Trivial-program reference: shows the form's overhead floor.
+
+(module hello
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body (do io/print_str "Hello, AILang."))))
diff --git a/examples/list_map_poly.ailx b/examples/list_map_poly.ailx
new file mode 100644
index 0000000..75f4ffd
--- /dev/null
+++ b/examples/list_map_poly.ailx
@@ -0,0 +1,59 @@
+; Iter 14b design exhibit — Decision 6 form (A).
+; Companion to box.ailx. Same hash-equivalence gate in Iter 14c.
+
+(module list_map_poly
+
+  (data List (vars a)
+    (doc "Singly-linked polymorphic list.")
+    (ctor Nil)
+    (ctor Cons a (con List a)))
+
+  (fn inc
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params x)
+    (body (app + x 1)))
+
+  (fn map
+    (doc "Apply f to every element. Recursive on the tail.")
+    (type
+      (forall (vars a b)
+        (fn-type
+          (params (fn-type (params a) (ret b))
+                  (con List a))
+          (ret (con List b)))))
+    (params f xs)
+    (body
+      (match xs
+        (case (pat-ctor Nil)
+          (term-ctor List Nil))
+        (case (pat-ctor Cons h t)
+          (term-ctor List Cons
+            (app f h)
+            (app map f t))))))
+
+  (fn print_list
+    (type
+      (fn-type
+        (params (con List (con Int)))
+        (ret (con Unit))
+        (effects IO)))
+    (params xs)
+    (body
+      (match xs
+        (case (pat-ctor Nil)
+          (lit-unit))
+        (case (pat-ctor Cons h t)
+          (seq
+            (do io/print_int h)
+            (app print_list t))))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (app print_list
+        (app map inc
+          (term-ctor List Cons 1
+            (term-ctor List Cons 2
+              (term-ctor List Cons 3
+                (term-ctor List Nil)))))))))