How Glyph is hardened
A language whose whole pitch is “your agents can't quietly break it” has to earn that. So we run fleets of AI agents that role-play skeptical engineers (a frustrated React developer, a backend contrarian, a safety adversary), have them build real apps and try to break the guarantees, then fix everything they surface. Here is that loop, and exactly what it found.
tsc --strict
Each is two files: a .ts that type-checks clean under
tsc --strict, and the same program in Glyph that does not
compile. A build gate re-runs all five and fails if either half stops
behaving, so a guarantee that quietly disappears takes the build with it.
catches: 5/5 verified both ways (verifiability: 5, greppability: 0, abstraction: 0, diff stability: 0). TypeScript checked with tsc --strict and @types/node 26.6.6.
| Glyph says | What TypeScript let through | Files |
|---|---|---|
E0200 | A case added to a union, and one handler that forgot it | catches/non-exhaustive-match/ |
E0224 | A read from a map, typed as if the key were always there | catches/absent-map-key/ |
E0230 | A string split into two names, when it may have no separator | catches/split-into-a-pair/ |
E0304 | A validator that reports success for a socket it never checked | catches/unverifiable-parse/ |
TS2322 | A parsed body assigned to a typed name without being checked | catches/unvalidated-boundary-read/ |
All five are verifiability. None of them is evidence for greppability,
abstraction or diff stability, and the gate prints those zeros. Four
earlier cases were dropped before the launch because TypeScript catches
them too, or because the two halves were not the same program;
catches/README.md says which and why.
The map read is refused even when the key is spelled right, because a
Record<string, string> says nothing about which keys
exist. TypeScript catches it with noUncheckedIndexedAccess,
which --strict does not turn on. The missing union case can
be caught in TypeScript too, with typescript-eslint's
switch-exhaustiveness-check or an assertNever
default, if the project adopts them. In Glyph neither check is optional.
The last one is refused by tsc, not by Glyph's own checker,
which misses it today (G289). glyph build type-checks the
TypeScript it emits, and there json.parse returns a
Result, not a User. TypeScript's
JSON.parse returns any, and the annotation on
user launders it.
Every finding is reproduced against the compiler, fixed at the root, and independently re-verified before it counts.
Persona agents build real programs (forms, backends, stateful UI) and record every place the language fought them.
Each finding is minimized to the smallest failing program and re-run against the compiler. Anything that can't be reproduced is dropped.
Root-cause fix in the Rust compiler with a regression test that fails before and passes after. The full suite must stay green, or the change reverts.
An independent pass re-runs every repro against the freshly built compiler, catching “the agent thought it was fixed” gaps before anything ships.
Each of these compiled clean and could ship wrong code that passed the type check: exactly the class of bug Glyph exists to prevent. Every one is now caught at compile time.
Result matchA match over Result<T, Empty | BadQty(...)> lowered to two
duplicate case "Err" branches; the first swallowed every error and
silently dispatched to the wrong arm.
Now: one grouped case with a correct inner switch; each variant routes right.
A typo'd variant in a match arm (Loded for Loaded) was silently
bound as an irrefutable catch-all, masking non-exhaustiveness and misrouting at runtime,
with no diagnostic.
Now: an unknown constructor is rejected at the typo, like a real name.
bool match slipped past exhaustivenessmatch n > 0 { true => ... } (missing the false arm)
compiled and passed tsc, then threw at runtime.
Now: a compile-time non-exhaustive-match error.
component C(a, b) emitted positional params, but React calls components
props-first, so a silently bound to the whole props object. It passed
tsc.
Now: a clear compile error pointing to the single props-record form.
<match> skipped exhaustivenessA JSX <match> with a missing <case> compiled green and
threw at runtime, unlike value-level match, which was checked.
Now: the same exhaustiveness check applies; a missing case is a compile error.
Binding a record-payload variant to a name (BadQty(b)) read a nonexistent
.value off the flattened payload.
Now: the payload binds correctly, so b.sku works.
Soundness the compiler used to leave to tsc, now caught by Glyph itself.
Too few or too many arguments were accepted (and ran to NaN). Now
E0213 rejects a wrong argument count.
? error type, across the stdlib boundaryThe exact-error-type rule was skipped when the error came from a stdlib wrapper. Now it's enforced there too.
owned handlelet g = f on a resource handle created a second binding that could double-close.
Now rejected (E0215).
An arm after a catch-all is now flagged; json.parse<T> now structurally
validates Record fields instead of only checking presence.
The small things that made a bad first impression, none of which served any purpose.
aria-label and data-* parsed as subtraction. Now they work, and
emit as proper React props.
Hyphenated and scoped specifiers (react-hook-form,
@hookform/resolvers/zod) were rejected. Now they import directly.
The runtime bootstrap wasn't loaded in a browser build, crashing on first run. Every emitted module now pulls it in.
Writing if now points at match; a range pattern says so directly;
JSX whitespace and a bare $ in text are handled.
Hardening means naming what isn't done, too. These are known and tracked, not hidden.
Deliberately deferred or awaiting a design decision:
Rejecting implicit-any closures in Glyph's own checker needs contextual
inference to avoid false positives on validly-typed callbacks.
Ergonomic FFI, using a complex-typed TS library without a per-library adapter, is the
largest interop question still open, tracked in
open questions.
A map that arrives from another module or the standard library is still read unchecked,
so E0224 does not yet reach a sqlite.Row, and the two-binding
for i, x in xs still loses its element types.