What a Type System Actually Proves
A type system is a lightweight proof system running on a decidability budget. What it proves is a theorem you can state; what it declines to prove is a design decision, not an oversight.
What properties can a type system actually prove about my program before it runs, and what is it structurally unable to prove?
The program as a set of *typing judgments*: one per expression node, each of the form “under these assumptions, this expression has this type”. The question this form exists to answer is not “what type is this” but “does a derivation exist for every node in the tree?” If one does, a specific, enumerable set of runtime states has been shown unreachable — and the size of that set is exactly the strength of the type system.
The checker may assume only what earlier phases established: the tree is syntactically well-formed, and [[name-resolution]] has bound every identifier to a declaration. It may not assume anything about any particular execution. A typing rule that held only for some inputs would not be a rule — judgments quantify over all runs, which is why a branch that never executes is checked exactly as hard as one that always does.
Key points
- A type system is a decidable proof system; checking is proof search, and acceptance is a statement about every execution, not about the runs you tried.
- Soundness is progress plus preservation: a well-typed program never reaches a state the semantics has no rule for.
- The whole content of the theorem is the definition of “goes wrong”, and that set is chosen by the designer.
- Rice’s theorem forces conservatism: every type system rejects correct programs, and the ones it rejects are the price of terminating.
- Expressive power, checking cost and annotation burden are three dials on one budget; you cannot move one without moving the others.
- The theorem leaks in exactly three places: deliberate unsoundness, escape hatches, and boundaries where data was never checked.
- Parse at the boundary so that later code is covered by the theorem again; validating and passing the raw value on covers nothing.
It is a proof system, and the theorem is short
The useful framing is not “types catch bugs”. It is: a type system is a decidable, syntax-directed proof system, and type-checking is proof search. When the checker accepts a program it has constructed a derivation. When it rejects one it has shown that no derivation exists under its rules. Both outcomes are statements about *every* execution of the program, which is what separates a type system from a test.
The theorem the derivation buys you is usually stated as two halves, due to Milner and sharpened by Wright and Felleisen. Progress says a well-typed expression is either finished or can take a step. Preservation says taking a step does not change the type. Together they say: a well-typed program never reaches a state the semantics has no rule for — it never “goes wrong”.
Everything interesting is hiding in the definition of “goes wrong”. That set is chosen by the language designer. In a typical ML it contains applying a non-function and adding a string to an integer. It does not contain dividing by zero, indexing past the end of an array, or exhausting the stack — those are given defined behavior (an exception, a panic, a trap) precisely so that they stay inside the theorem. Widening the set is what [[nullability]], [[exhaustiveness-checking]] and [[ownership-types]] each do, one class at a time, and each widening is paid for somewhere.
Progress If ⊢ e : T and e is not a value,
then there is some e′ with e → e′
(a well-typed program is never stuck)
Preservation If ⊢ e : T and e → e′,
then ⊢ e′ : T
(evaluation does not change the type)
Together A well-typed program never reaches a state
for which the semantics defines no next step.
Read ⊢ e : T aloud as "e has type T".
Read e → e′ aloud as "e steps to e-prime".The decidability budget
Rice’s theorem says every non-trivial semantic property of programs is undecidable. A type checker must terminate, so it cannot decide any interesting property exactly. It therefore approximates conservatively: it accepts a subset of the programs that would actually have behaved, and rejects the rest. Every rejected-but-correct program is the budget being spent.
That gives three dials the designer trades against one another, and moving any one of them moves the others. Expressive power: how many correct programs are accepted. Decidability and cost: whether checking terminates, and in what time bound. Annotation burden: how much the programmer must write to help. Full dependent types (Agda, Idris, Lean, F*) buy enormous expressive power and pay in both of the others; Go’s type system buys fast checking and cheap annotations and pays in what it can say.
The table below is the honest version of “what do types give me”. Read the last column: nothing in it is free, and every row that a mainstream language declines to prove was declined on those grounds, not by accident.
| Property | Proved where | What it costs to prove | Left unproved by mainstream systems |
|---|---|---|---|
| Operator/operand compatibilitytypical | Almost every static system | Little — this is the cheapest rule set there is | — |
| Every case is handledspec | ML, Haskell, Rust, Swift, TS unions | The type must be a closed sum; adding a case must break every match — see [[exhaustiveness-checking]] | Open hierarchies and enums that grow across versions |
| A reference is never absentimplementation | Kotlin, Swift, Rust, TS strictNullChecks | Every optional value needs an explicit unwrap at the use site — see [[nullability]] | Java, C#, Go, C++ raw pointers |
| No use after free, no double freeimplementation | Rust’s borrow checker | A whole extra analysis, lifetimes in signatures, and rejection of correct aliasing patterns — [[ownership-types]] | Every garbage-collected language answers this at runtime instead |
| No data race on shared stateimplementation | Rust (Send/Sync), Pony | The same borrow discipline extended across threads, plus auto-trait leakage across API boundaries | Almost everything else; the Concurrency domain owns data races themselves |
| Which effects a function may performtypical | Koka, Eff, Haskell’s IO, checked exceptions | Effect annotations propagate up every caller — [[effect-systems]] | Java abandoned it in practice; most languages never tried |
| The function terminatesspec | Agda, Idris, Coq, Lean | A termination checker that rejects perfectly good recursion it cannot see through | Every general-purpose language, deliberately |
| The function computes the right answerspec | Dependently typed languages, with proof obligations | You write the proof. This is the far end of the budget. | All of them |
Three ways the proof leaks
any, unchecked index signatures. This is true of TypeScript as shipped through the 5.x line; the strictFunctionTypes flag closes exactly one of these holes for standalone function types and deliberately not for methods. Kotlin, Swift and Rust make the opposite bargain in the same places and pay for it in ceremony at the boundary.A theorem holds under its hypotheses. In a real language the hypotheses are violated in three predictable places, and knowing which one you are standing in is most of the practical skill.
Deliberate unsoundness. Some rules are known-wrong and kept for compatibility or ergonomics. Java’s covariant arrays are the textbook case and are the subject of [[variance]]. TypeScript’s bivariant method parameters and its any are documented non-goals of soundness. These are not bugs; they are priced decisions, and the price is paid at runtime.
Escape hatches. any, unsafe, unchecked casts, reflection, Object, interface{}, void*, and every deserializer. Inside the hatch the checker has stopped reasoning, so the theorem covers everything except the part of the program where the data comes from.
Boundaries. The proof is about the program. Bytes arriving from a socket, a database driver, an environment variable or a model response were never checked by it. This is why the discipline that matters at the edge is parse, don’t validate: convert untrusted input into a type whose existence *is* the evidence, once, at the boundary, and let the rest of the program be covered by the theorem again. Doing the reverse — checking a shape and then passing the unrefined value onward — leaves every later function relying on a proof nobody holds.
- Ask of any type system: what is in its “goes wrong” set? That is the theorem, and everything outside it is still your problem.
- Ask where the hatches are. A codebase’s real type discipline is the density of
any,unwrap,as, andinterface{}at its boundaries. - Ask whether the boundary parses or merely validates. Only one of the two produces a value the checker can reason about afterwards.
- A system can be sound and useless (reject everything) or unsound and beloved (TypeScript). Soundness is a property, not a score.
Writing the theorem down for your own language
If you are designing a language or a schema layer, this lesson has one deliverable: a sentence of the form “a well-typed program in this language never ___”. If you cannot finish that sentence, you have a set of annotations, not a type system, and you will find out which at runtime.
The sentence also tells you where the tests go. Anything not in the blank is uncovered, and the parts a type system cannot reach — resource exhaustion, wrong arithmetic, wrong business rule, wrong ordering under concurrency — are precisely the places a test suite earns its keep. The two are complements, and a team that argues about which is “better” has not written the sentence.
The same discipline transfers directly to agent and API work. A JSON schema on a tool call is a type system with a very small theorem: it proves shape and, if you use enums, membership. It proves nothing about whether the arguments are *permitted* — and treating schema conformance as authorization is the failure mode [[typed-tool-calls]] and [[plan-validation]] exist to prevent.
How it works
The steps, in the order the compiler takes them.
- Name resolution completes, so every identifier in the tree points at a declaration and every declaration carries a written or inferrable type.
- The checker walks the tree and, at each node, looks for a typing rule whose premises it can satisfy from the children’s types.
- Satisfying a premise may require recursing into a child (synthesis), or checking a child against an expected type pushed down from the parent (checking).
- Rules that need unknowns generate constraints instead of answers; those are solved by
[[unification]]and folded back in. - If every node gets a type, the derivation is complete: the tree is annotated and handed to lowering as a typed AST.
- If some node has no applicable rule, the checker reports the failure — and choosing *which* node to blame is the entire difficulty of
[[diagnostic-quality]]in a type checker.
How it breaks
What the engineer observes when it goes wrong — not what goes wrong internally.
- The program compiles cleanly and throws at runtime anyway, and the engineer concludes the type system is broken. It is not: the failure class was never inside the theorem — a division by zero, an index out of range, a null arriving through a deserializer.
- A correct program is rejected and the engineer fights the checker for an hour. The conservatism is the design; the fix is usually to restructure so the property is visible to the rules, not to add a cast.
- A single
any,interface{}or unchecked cast at a module boundary silently un-types everything downstream of it, and a type error surfaces three services away as a JSON field that is a string where everyone assumed a number. - Type-checking time grows super-linearly on a generated or deeply generic file, and CI goes from two minutes to eleven with no runtime change at all.
- A schema-validated agent tool call is treated as an authorization check; the arguments are well-shaped and the action was never permitted.
- Two services agree on a type name and disagree on its meaning. Both type-check. The mismatch appears as data corruption, because a type name is not a shared theorem across process boundaries.
When it helps
- Deciding what a type annotation is worth on a specific boundary: if it moves a class of failure from runtime to build time for the whole codebase at once, it is worth ceremony that a local convenience is not.
- Evaluating a language for a project: read the “goes wrong” set rather than the marketing. Memory safety, exhaustiveness and null-absence are four different rows in that table and no language gives you all of them free.
- Arguing about test coverage productively. What the type system proves does not need a test; what it declines to prove needs one badly.
- Designing a schema or DSL, where the temptation is to keep adding validation rules instead of admitting you are building a type system and giving it a theorem.
When it hurts
- Exploratory and one-off code, where the annotation burden is paid up front and the refactoring safety it buys is never collected.
- Genuinely heterogeneous data — a config tree, a wire format that grew for a decade — where encoding the shape costs more than handling it dynamically and re-checking at each use.
- When the cost lands on the wrong people: a library author who must annotate variance and lifetimes so that call sites read cleanly is paying a real, unshared bill.
- When it becomes an identity rather than a tool, and the team spends a week making an inexpressible invariant expressible instead of writing the assertion.
What it costs
Every one of these is paid by something.
- Every property added to the theorem costs annotation burden at the places the checker cannot infer it, and costs rejection of correct programs at the places its approximation is coarse. Rust’s memory-safety proof is the clearest bill: signatures grow lifetimes and some correct aliasing patterns must be rewritten or moved behind
unsafe. - Stronger checking costs compile time and, at the far end, compile-time *complexity class*. ML-style inference is exponential in the worst case, C++ template instantiation is Turing-complete, and both are fine until a generated file makes them not fine.
- Soundness costs ergonomics and adoption. TypeScript reached the JavaScript ecosystem by being unsound on purpose; a sound gradual system would have had a fraction of the uptake and rejected a large share of existing code.
- A theorem stated in prose rather than formally costs you the ability to know it holds. Most industrial languages pay this willingly; the cost surfaces as unsoundness bugs discovered years later, in the wild.
What else you could do
What a different compiler or language does instead, and when that is better.
- No static type system at all, with runtime tagging and contract checks at boundaries. Smalltalk, Erlang, Clojure with spec: the checks are real, they are just placed at the boundary rather than over the whole program — see
[[static-vs-dynamic-typing]]. - Contracts and refinement checked at runtime — Eiffel’s preconditions, Clojure spec, Python’s
pydantic. They express properties no mainstream static system can, and they express them about the run that happened, not about all runs. - A separate static analyser rather than a type system —
[[static-analysis]]and[[abstract-interpretation]]prove things about programs a type checker has already accepted, at whole-program cost and with false positives a type system is not allowed to have. - Formal verification of the specific property that matters, leaving the type system small. seL4 and CompCert take this route: an ordinary type system plus a proof about the thing you actually care about — see
[[verified-compilers]]. - Gradual typing, which lets a codebase choose the boundary between the two answers file by file, at the cost of a runtime check at every gradual edge —
[[gradual-typing]].
See it for yourself
The flag, dump or tool that shows you this directly.
- Ask a checker what it proved:
tsc --noEmit --strictand then flip individual flags (--strictNullChecks,--noUncheckedIndexedAccess) to watch the theorem grow and the error count with it. mypy --strictversusmypyon the same Python file shows the same dial in a gradual system;--disallow-any-explicitshows you where the hatches are.grep -rn "\bany\b" srcandgrep -rn "unsafe {"are the fastest honest audit of where a codebase’s theorem stops holding.rustc --explain E0502(and any other error code) prints the rule that was violated and why it exists — the best in-toolchain writing on why a conservative rejection is conservative.ghci -XNoMonomorphismRestrictionand:type +vshow inferred types before and after generalization; useful for seeing what a system concluded rather than what you assumed.
Plausible wrong readings
Stated the way a confident engineer states them.
- “If it compiles, it works.” It means a derivation exists under the rules. Whether the program computes the right answer is outside every mainstream type system’s theorem, and always was.
- “Once it type-checks there is nothing left to test.” The type system and the test suite cover disjoint properties. Everything the checker declined to prove is the test suite’s entire job.
- “Any rejection is the type system getting in the way.” Some are. Most are the conservative approximation doing exactly what it was designed to do, and the restructure it forces is usually the fix.
- “A stronger type system is strictly better.” Stronger means more annotation, slower checking and more correct programs rejected. Better is whether that trade fits the codebase.
- “Types are documentation.” They are, but that is a side effect. They are first a claim the machine checks, and a documentation-only type — one nothing enforces at the boundary — is a comment.
Misconceptions
The claim, and what is actually true.
Go deeper
The same idea at increasing depth. Stop wherever it stops being useful.
overview
A type system is a set of rules the compiler uses to prove something about your program before it runs. The proof is real and it covers every possible execution, which is much stronger than a test. But it only covers the property the language designer chose, and that property is usually narrow: operands fit their operators, functions are called with what they asked for. Wrong answers, missing data and exhausted resources are outside it. Learn the sentence “a well-typed program in this language never ___” for whichever language you are using; the blank is what you get.
practical
On a real codebase the leverage is at the three leak points, not in the middle. Audit where any, interface{}, unsafe, reflection and deserializers appear — those are the places the theorem stops. Convert boundaries so they produce a domain type rather than validating and passing the raw value on; every function downstream then gets the guarantee for free. When the checker rejects something correct, prefer restructuring so the property is visible over adding a cast, because a cast moves the failure to runtime and moves it away from the line that caused it. And when you argue for a stricter flag, argue in the currency: which class of failure moves to build time, and what annotation bill does the team pay for it.
advanced
The design question is where to spend the budget, and the interesting observation is that the three dials interact non-linearly. Adding subtyping is cheap in annotation and expensive in inference — it destroys principal types, which is why [[hindley-milner]] cannot absorb it. Adding overloading is cheap in ergonomics and expensive in resolution, which becomes search. Adding ownership is expensive in annotation and buys a property nothing else on the list can buy. Notice also that the choice constrains the back end: a system that proves types statically and erases them enables unboxed layout and direct calls, while one that keeps tags enables [[inline-caches]] and speculation instead. The type system is not only a frontend concern — it is the single largest input to what the code generator is allowed to assume.
internals
A soundness proof for a real language is a substantial artifact and the places it is hard are informative. Mutable state breaks naive generalization, which is why ML needs the value restriction ([[hindley-milner]]). Subtyping plus mutable containers breaks the obvious variance rules, which is why [[variance]] exists and why Java patched it with a runtime store check. Erasure plus reflection breaks parametricity, which is why Java has heap pollution warnings. In each case the pattern is the same: a feature added for ergonomics invalidates a hypothesis of the theorem, and the language either restricts the feature, adds a runtime check, or accepts the hole and documents it. When you meet an odd rule in a type system, assume it is the scar tissue from one of these three responses and go looking for which.
How much this depends on
Nothing in this domain is true of every compiler. These say how much.
strictFunctionTypes, and index access is unchecked unless noUncheckedIndexedAccess is on. Kotlin and Swift close the null hole and leave others open. Read each language’s own list; there is no shared default.unsafe blocks carries the obligation manually, and a soundness bug in a widely used crate un-types every dependent.If you were asked this in an interview
- State what a well-typed program in your main language is guaranteed not to do. Now state three things it is not guaranteed about.
- Why must every type system reject some programs that would have run correctly?
- TypeScript is unsound on purpose. Name one place, and say what was bought with it.
- Where in your codebase does the type system stop reasoning, and what would it take to move that boundary outward by one layer?
Connections
- Testing & Reliability Engineering — What to test once you know what the type system provedThe two are complements: the type checker covers all executions of a narrow property, a test covers one execution of an arbitrary property. Deciding the split is a testing-strategy question, and the reasoning about what is left uncovered belongs there.
- Programming Languages & Runtime Internals — Runtime type tags, object headers and dynamic dispatchThis lesson is about what is proved before execution. What a value carries with it at runtime — a header, a class pointer, a hidden class — is the runtime’s half of the same subject, and the two designs constrain each other.