correct the architecture docs against what was measured
capabilities.md cited '== lowering to str_eq unless both operand names are in a hardcoded int-name set' as the paradigm defect. That is wrong: __int_names comes from type annotations, which is legitimate propagation. The real defect was 35 hardcoded builtin return types one layer down, and mislocating it hid a live miscompilation of unannotated lets. geometry-vs-code.md listed concurrency and error handling as open. Both are answered: ordering is a partial order and coordination is the price of forgetting; standing is signed, so not-known and known-false are opposite directions rather than one boolean. Added the fourth proof form (adversarial exactness) and recorded that form 1 no longer survives as a verdict -- every row it justified was a basis, not a capability. Also marked cross-cutting concerns as implemented rather than predicted.
This commit is contained in:
@@ -6,8 +6,19 @@ This list is the unit of analysis. Each entry gets one question — *prove this
|
||||
cannot be done with pure geometry* — and the answer determines whether it stays a
|
||||
capability of the language or collapses into the manifold.
|
||||
|
||||
Draft, 2026-08-17. Not yet audited. Ordered roughly from most-likely-geometry to
|
||||
most-likely-code.
|
||||
Draft, 2026-08-17. Ordered roughly from most-likely-geometry to most-likely-code.
|
||||
|
||||
**Status after measurement.** The list was audited against the implementation
|
||||
the same day. 28 entries collapsed to 19 geometry + 3 code: serialization, text
|
||||
encoding, network and emission are all *projection onto a basis* (row 18) —
|
||||
the convention is the basis, never the act. Storage collapsed because
|
||||
persistence has no caller. Concurrency collapsed because coordination is the
|
||||
price of forgetting, not a capability. A fourth proof form was added,
|
||||
**adversarial exactness**, and form 1 stopped being a valid verdict.
|
||||
|
||||
**The table answers CAN only.** SHOULD and COST resolve per *site*, not per
|
||||
capability — `is_digit` and `is_letter` are one capability with opposite
|
||||
answers, and comparison spans three cost tiers. See the notes below.
|
||||
|
||||
---
|
||||
|
||||
@@ -83,8 +94,37 @@ match-strength field: first zero, all zeros, last zero, count of zeros, first
|
||||
class-crossing. One relation, five functions.
|
||||
|
||||
**14 — Selection is the crux for the compiler.** `+` dispatching on AST node kind
|
||||
and `==` lowering to `str_eq` unless both operand names are in a hardcoded int-name
|
||||
set are both selection-by-enumeration where selection-by-position belongs.
|
||||
is selection-by-enumeration where selection-by-position belongs.
|
||||
|
||||
**Correction, 2026-08-17, from measurement.** This entry previously also cited
|
||||
`==` lowering to `str_eq` "unless both operand names are in a hardcoded int-name
|
||||
set — a literal list of variable names treated as integers." That is **wrong**.
|
||||
`__int_names` is populated from *type annotations* (`param["type"] == "Int"`,
|
||||
`let x: Int`), which is primitive but legitimate type propagation, not an
|
||||
enumeration of blessed variable names.
|
||||
|
||||
The real defect was one layer down: `is_int_call` held **35 hardcoded builtin
|
||||
return types**, the same shape as the 19 temporal ones. Those moved to
|
||||
`lang/tools/check/signatures.rel`.
|
||||
|
||||
And the mischaracterisation hid a live bug. Because the return types were never
|
||||
consulted at a *binding* site, an unannotated `let` lost its type:
|
||||
|
||||
```el
|
||||
let a = str_len("hello") // no annotation
|
||||
let b = str_len("hi")
|
||||
let c = a + b // → el_str_concat(a, b) on two integers
|
||||
```
|
||||
|
||||
That compiled clean, ran, and printed nothing where it should print 7 — no error
|
||||
at any layer. Present in the pre-change compiler, so pre-existing. Fixed by
|
||||
taking an unannotated `let`'s type from what its initialiser returns; the data
|
||||
was already required for dispatch and simply never read there.
|
||||
|
||||
**The general lesson, since it recurred all session:** the enumeration was real
|
||||
but I had located it in the wrong place. Naming a defect from reading is a
|
||||
hypothesis. Eight hours of reading this file did not surface the miscompilation;
|
||||
moving the data out and running the result did.
|
||||
|
||||
---
|
||||
|
||||
|
||||
Reference in New Issue
Block a user