diff --git a/docs/architecture/capabilities.md b/docs/architecture/capabilities.md index fcce174..277b659 100644 --- a/docs/architecture/capabilities.md +++ b/docs/architecture/capabilities.md @@ -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. --- diff --git a/docs/architecture/geometry-vs-code.md b/docs/architecture/geometry-vs-code.md index eedf6e2..15a7a5a 100644 --- a/docs/architecture/geometry-vs-code.md +++ b/docs/architecture/geometry-vs-code.md @@ -43,7 +43,7 @@ correcting. | Self | a world-tube — a trajectory through the manifold | | Consolidation | episodic → semantic promotion | | Reification | dense regions cohering; runs on the beat, has no caller | -| Cross-cutting concerns | **dissolved** — a hold is a *neighbour*. Adjacency, not tracking | +| Cross-cutting concerns | **dissolved** — a hold is a *neighbour*. Adjacency, not tracking. **Implemented 2026-08-17**: a construct declares what runs at a crossing, and it resolves at execution — see the runtime seam. | | Effects | topology. `reach_out` is bounded by `detect_gap` and `verify` because those are its edges | | Capability | position relative to a boundary. In C it is already spelled `const` | | The AST | a projection of geometry into a tree — a surface, not the centre | @@ -58,7 +58,7 @@ correcting. | CRC32 polynomial, Adler32, zlib framing | same — agreed constants, derivable from nothing | | Cosine, distance, the float arithmetic | the machinery that *walks* the geometry is not itself geometry | | Arena, refcount, allocator | bookkeeping for the **representation**, not for the positions | -| Locks, threads, publication boundary | hardware concurrency has no geometric analogue | +| Locks, threads, publication boundary | the hardware is code. **Ordering is not** — see Answered, above. Coordination is required only where state is non-monotone. | | WAL, page layout, ARIES recovery | durability against a physical device that can lose power | | Emission — writing C or JS text | the final surface has to be *typed out* by something | | OS interaction — launchd, spawn, signals | outside the system by definition | @@ -90,12 +90,32 @@ column. --- +## Answered + +| Thing | The answer | +|---|---| +| Concurrency | **Ordering is geometric.** Causality is a partial order (Lamport 1978); a total order is an arbitrary extension of it and "cannot be depended on to imply a causal relationship." Programming languages force you to write a total order, so authoring *invents* constraints the problem never had — and every lock, barrier, fence and consensus protocol is apparatus for recovering the partial order destroyed at authoring time. CALM (Hellerstein/Alvaro, proven by Ameloot et al.): a program has a consistent coordination-free implementation **iff it is monotone**. What breaks monotonicity is destructive update. **Coordination is the price of forgetting.** | +| Error handling | **`grounded: false` covers not-knowing; it does not cover failed.** Standing is a *signed* component: `> 0` supported, `= 0` unknown, `< 0` contradicted. Not-known and known-false are opposite directions on one axis and a boolean cannot tell them apart. `inhibitory` as an int32 flag is that sign wearing a boolean. | + +## Fourth proof form + +**4 — ADVERSARIAL EXACTNESS.** Where approximation is a break, geometry is +excluded. A cryptographic hash is a *deliberately structure-destroying* map: +near inputs land at maximally uncorrelated outputs. Geometry is the claim that +near things stay near — a manifold that approximated SHA-256 would *be* a break +of SHA-256. Signature verification is the same: 0.99-valid is invalid. And +X25519 **is** geometry, a group on an elliptic curve, which is precisely why it +must be code: its security is the hardness of moving in that geometry. + +**Form 1 no longer survives as a verdict.** Every row it justified turned out to +be a *basis*, not a capability. RFC 8259 fixes where the commas go — that is a +surface, and projecting onto a surface is geometry. A convention describes the +basis you project onto; it never describes an act. + ## Open — not yet decided | Thing | The question | |---|---| -| Concurrency | hardware threads are code, but is *ordering* geometric? | | Parsing | is a grammar a convention, or a region? | | The module system | if the partition is a neighbourhood, does linking survive? | | Numeric literals | is `3` a position, or a convention we agreed on? | -| Error handling | `grounded: false` covers not-knowing. Does it cover *failed*? |