Gradual typing and blame — the soft/hard seam has a theorem

Parent: recursive-harness

Another instance of softened logic with a harness payoff — the softening of TYPE SYSTEMS, and it brings a theorem we've been missing. When you stop asking "typed or untyped?" and start asking "how confident is this boundary?", a classical result from programming language theory snaps into focus.

The softening: gradual typing — Siek–Taha (2006)

The hard question: can typed and untyped code share a program? Classical answer: no — either the whole thing is statically checked (safe but rigid) or it's dynamic (flexible but fragile). Gradual typing's insight is to refuse the dichotomy. Instead: let both exist in one program, and every boundary crossing gets a runtime cast that checks the value as it passes.

The typed side makes guarantees; the untyped side makes none. At the seam, a runtime check (the cast) either confirms the value matches the type or rejects it. Not typed-or-untyped (hard partition) but a spectrum with checked seams (soft transitions). The cast is the only new mechanism — everything else is standard.

The mapping — a harness IS a gradually-typed program

Artifacts begin as untyped — LLM freeform text, code, whatever emerges. Progressively, they harden: you write a spec for a subtree, a test harness runs, a mechanical gate checks the result. Every soft→hard crossing is a cast, and a cast is a gate (gate-theory). The writable/tacit seam where human and harness negotiate is exactly the typed/untyped boundary: the human side writes freeform, the mechanical side checks it against a spec before it goes downstream.

This is not metaphor — the category structure is identical. A gradual type system is a harness for source code; a harness is a gradual type system for AI artifacts.

The theorem we get: blame — Wadler–Findler's blame calculus

When a cast fails, who is responsible? A classical theorem: "well-typed programs can't be blamed." When a runtime check fails at a boundary, blame is assigned MECHANICALLY — not by heuristic, not by a judge, but by traversing the provenance: the untyped side of that boundary is charged. You trace blame backward through failed casts until you reach the last mechanical gate that passed (or the freeform source if no gate passed). That location is the culprit.

Harness translation: A subtree behind mechanical gates cannot be the culprit. When something breaks downstream, blame flows backward through provenance edges to the lowest-confidence crossing. Culprit assignment stops being a heuristic and becomes a calculus. This sharpens modal-status-labels's confidence axis into a blame-ordering: we know not just that a subtree is uncertain, but which upstream crossing to blame first.

The honest caveat: semantic gates have imperfect casts

The blame theorem assumes casts are perfect — a value either passes or fails, no ambiguity. Reality: semantic gates are opaque. A gate with measured tolerance α can pass a bad value (with probability ≤ α) and then blame points one boundary too far downstream. So blame conclusions inherit the confidence ledger: "cannot be blamed, with confidence 1−α of its gates." Each gate in the chain from culprit to failure subtracts its error from your confidence.

This is not a flaw — it is what operationalizing-tolerances means. Blame is only as sharp as your gates are.

One line

The soft/hard seam isn't just where checks live — it's where blame is decided, and behind a mechanical gate you are provably innocent (up to the gate's measured α).