Files
el/docs/v1/experiments/cycles/17-annotations-are-never-checked.md
T
bigmerge c6ba0677f0 log v1 experiments: nineteen cycles, organised by the method that produced them
cycles/    one file per Ishikawa -> scientific method -> Six Sigma loop, named
           for the DEFECT not the fix, carrying the commit record as written at
           the time
findings/  what the cycles produced, cross-cut: live bugs, architecture answers,
           and defects in my own measurement

The organising finding is that predictions which came back FALSE produced every
significant result. Eleven of sixty-one failed, and those eleven found: that the
arity table was not drifted but 40% incomplete; that the AST traversal is
irreducible and only rules and judgments move; that guards could refuse through
the seam after all; and that routing el_bin_lookup through the gate did NOT fix
the SIGSEGV, because the fallback strlen was the hazard -- a wrong fix I would
otherwise have shipped as verified.

One cycle was run without committing predictions first and had to be discarded
as rigged. It is kept, in full, as 18-async-half-expressible.md.
2026-08-17 10:52:17 -05:00

2.2 KiB

annotations are never checked

Status: verified on experiment/annotation-checking, not merged.

Ishikawa — why does El silently miscompile?

Three bugs found the same day shared one shape.

method       type tracked by per-function name sets, fed from annotations
machine      el_val_t erases everything at the C boundary
material     no propagation through expressions
measurement  nothing verifies an annotation against what it annotates
─────────────────────────────────────────────────────────────────────────
root cause   El has type ANNOTATIONS but no type CHECKING. The annotation
             feeds dispatch and is never itself verified.

Predictions

P1  let x: Int = "hello"  compiles clean               expect TRUE
P2  let s: String = 42    compiles clean               expect TRUE
P3  the annotation drives dispatch, unverified         expect TRUE
P4  same root cause as all three bugs found today      expect TRUE
P5  checking literal-vs-annotation catches both        expect TRUE
P6  zero false positives across the compiler's source  expect TRUE

Results — 6/6, and worse than a wrong answer

let x: Int = "hello"; x + 1     →  4343631981   a string POINTER used as an integer
let s: String = 42; println(s)  →  nothing      address 42 dereferenced as a string

The first leaks a raw memory address into program output. The second is an arbitrary-read primitive if that integer is ever attacker-influenced.

Verified: 6/6, zero false positives across the compiler's own source, fixpoint ok, 105/105 native.

Six Sigma

The emitter only records the mismatch; tools/check/annotations.sh decides — consistent with every other check. Literals are checked because they are unambiguous.

Incomplete, stated not hidden: only literals. let x: Int = some_string_fn() still passes, because signatures.rel carries Int/Instant/Duration and no String entries. That is a data gap, not a capability limit — every El function declares its return type in source and codegen already holds ret_type on every FnDef.