Pillar 01 · The wedge
Verifiability
Glyph closes the holes an agent falls through: there's no any and no
as you can write, match is provably
exhaustive, and the types you declare get strict runtime validators
— all enforced as a strict layer on top of tsc. It doesn't verify
everything itself, and it's honest below about exactly where the guarantee stops.
The lie a type can tell
In TypeScript a type is a compile-time promise that evaporates before your code runs. A
User annotation is erased to nothing; the object you actually get from a
network call, a JSON parse, or a form field could be any shape at all. Worse, the language
hands you three legal ways to lie to the checker about it: any, an
as cast, and a non-null !. An agent working fast reaches for all
three — and tsc --strict stays green while the bug ships.
Glyph's first job is to close those holes. Not with more annotations, but by removing the escape hatches and making every type carry its proof to runtime. Here is what that means, one guarantee at a time.
01 There is no any
any is the single most expensive keyword in TypeScript: it switches off the
type system for a value and everything that value touches. One any at
a boundary quietly poisons the call graph downstream. Glyph doesn't have it. The top type is
unknown, and unknown is inert — you cannot call it, index it,
or pass it anywhere typed until you have proven what it is.
function handle(body: any) {
// tsc --strict: fine.
// runtime: throws on {}.
return body.user.name.toUpperCase();
}
fn handle(body: unknown) -> string {
return match User.parse(body) {
Ok(u) => string.upper(u.name),
Err(_) => "unknown",
}
}
You cannot get a typed value out of unknown without a check the compiler can
see. In Glyph, the narrowing is the runtime proof — there is no
syntax for skipping it.
02 Types are real at runtime
How does User.parse exist? Because every non-generic record type generates a
runtime descriptor alongside it — an is guard, a
parse that validates an unknown into a Result, and a
composable schema. The record's shape is actually inspected at runtime, not
assumed — so an is User check is a real check, not an erased no-op.
type User = {
id: number,
name: string,
email: string,
}
// generated: User.is(v), User.parse(v) -> Result<User, ...>, User.schema
fn create(req: Request) -> Result<Response, string> {
return match User.parse(req.body) { // untrusted input, validated
Ok(user) => Ok(json(201, user)),
Err(issues) => Ok(json(400, issues)),
}
}
This is the answer to "every API needs a hand-written validator." The type is the validator. A boundary — a request body, a config file, a third-party response — becomes typed only by passing through a check that can actually reject bad data.
The honest edge: descriptors are generated for non-generic record types
today, and a record's check is strict by default — it confirms the declared fields
and rejects a value carrying undeclared keys (an @open type opts out).
What's still on the roadmap is coverage: a generic envelope (Paginated<T>),
a union, or a type imported from a .d.ts doesn't get a descriptor yet. Where a
check can only prove part of a shape, the compiler is being taught to say so rather than
imply a guarantee it can't make.
03 Every case, or it doesn't compile
A match over a sealed union must handle every variant. Add a variant later and
every match that didn't account for it stops compiling (E0200) —
the new case cannot silently fall through to undefined the way a forgotten
switch branch does. And it isn't only unions: matching a number or
string on literal values requires an else (E0218),
because those domains are unbounded and a set of literals can never be complete.
type Status = Active | Paused | Cancelled
fn label(s: Status) -> string {
return match s {
Active => "on",
Paused => "hold",
// forgot Cancelled...
}
}
[E0200] non-exhaustive match on `Status`: missing variant `Cancelled` # the equivalent TS switch returns # undefined at runtime and compiles # clean. here it does not build.
04 Errors are values, not surprises
A function that can fail returns Result<T, E>. You handle it with
match, or propagate it with the ? operator — and the error
type has to line up (there is no implicit conversion hiding a mismatch). Ignore a
Result entirely — call it for effect and drop what it returned —
and Glyph warns you (E0217), because a discarded error is a swallowed failure.
You silence it deliberately with let _ = ..., never by accident.
fn load(id: string) -> Result<User, AppError> {
let raw = fetch_user(id)? // Err short-circuits to the caller
let user = User.parse(raw.body)? // validation Err propagates too
return Ok(user)
}
fn main() -> number {
save(user) // E0217: this returns a Result whose Err is dropped
return 0
}
05 Even PII is type-level
The same "make it the compiler's job, not a convention" instinct reaches all the way to
sensitive data. Put @redact on a type and its descriptor gains a
redact() that masks those fields, so a stray
json.stringify(User.redact(u)) can't leak them. Name a field the type doesn't
have and it's a compile error (E0219) — not a redaction that silently
protects nothing.
@redact fields: [diagnosis, notes]
type Patient = {
name: string,
diagnosis: string,
notes: string,
}
// json.stringify(Patient.redact(p)) ->
// {"name":"Ada","diagnosis":"[REDACTED]","notes":"[REDACTED]"}
Five different failure modes — unchecked input, a missed case, a dropped error, a leaked secret, an unvalidated key — and in every one the fix is the same shape: the compiler refuses to pretend.
How it's enforced — and where the guarantee stops
Being precise, because the difference matters: Glyph is a strict, enforced dialect
over tsc, not an independent verifier. Some things it proves itself
— exhaustiveness, the ? error type, the absence of any/as
in your source, strict-key validation. The rest of type compatibility it enforces by
emitting TypeScript and running tsc --strict, which fails the build. The wedge
is that these checks are the language, not opt-in lint the agent can disable —
not that Glyph re-implements a type checker.
Two earlier edges here were closed in 0.1.10. The emitter used to insert a
checked-by-Glyph-not-tsc return cast in every generic function; it now
fires only where a validator combinator assembles a value of a shape-derived type
(infer_shape<Shape>), and every honest generic emits with no cast at all.
And a validator's output type is no longer trusted: infer_shape derives it from
the shape you pass, and tsc checks your annotation against it — a shape
missing a field of the type you claim now fails to compile.
One edge remains, named plainly: a generic or imported field inside
T.parse is still runtime-checked only for presence, so T.parse is
fully sound for concrete record types and weaker for generic ones. Real descriptors for
generic and imported types are the top item on the roadmap, and until they land the
guarantee is exactly as strong as this says, not stronger.
The benchmark — coming
This claim is empirical, so we intend to measure it honestly: take a corpus of real
agent-authored changes, run each through tsc --strict and through Glyph, and
count what each one actually catches. Glyph isn't in real-world use yet, so there are no
numbers to report — the chart below is a placeholder, and it fills in with real data
the moment there is real usage.
tsc --strict vs Glyph
None of this is bought with ceremony. There are no proof annotations, no contracts, no verifier to satisfy — the code above is just ordinary Glyph. Verifiability isn't a feature you turn on; it's what's left once the ways to lie are gone.