Type Soundness
A type system is sound relative to its formal model if every accepted program preserves the typing guarantees that model defines. That is a much narrower claim than "no bugs", and several widely used type systems break it on purpose.
What does it actually mean for a type system to be "sound", and why is TypeScript deliberately not?
A pair of theorems over a formal model of the language: a syntax, a set of typing rules, and an operational semantics. The object of the proof is the model, never the implementation, so every soundness claim is relative to what the model includes — and the interesting engineering questions are usually about what it leaves out.
Later phases may assume exactly what the model proves and no more. An optimizer that relies on a value having its declared type is cashing in preservation; in a system with a deliberate unsoundness — a bivariant parameter, a covariant array store, a dynamic type — that assumption must either be backed by an inserted runtime check or abandoned. This is why some compilers for unsound systems emit checks that look redundant: they are the price of the hole.
Key points
- Soundness = progress + preservation, proved over a formal model of the language, and the claim is always relative to that model.
- "Well-typed programs do not go wrong" means they do not get stuck; what counts as stuck is decided by which steps the model defines.
- Soundness excludes a specific class of failure — an operation applied to a representation it was not defined for — and says nothing about wrong answers, non-termination, or resource exhaustion.
- A sound language can still panic, throw and deadlock, because those are defined steps rather than stuck states.
- Java's covariant arrays, TypeScript's bivariant method parameters and
any, and Dart'sdynamicare all deliberate holes with stated motivations. - A hole is paid for in one of two ways: an inserted runtime check, or an accepted gap that you must compensate for yourself.
- Unsoundness is not only aesthetic: an optimizer that trusts a type the value does not have is transforming a program it has misread.
What the claim actually says
The slogan is Milner's: "well-typed programs do not go wrong." Stated carefully, soundness is the conjunction of two theorems about a formal model of the language.
Progress: if a term is well-typed, it is either already a value or there is a step it can take. In other words a well-typed program never reaches a stuck state — a configuration that is not a result and where no evaluation rule applies. Preservation (or subject reduction): if a term is well-typed at type T and it steps to another term, that term is also well-typed at T. Types do not drift during evaluation.
Together they give an induction: a well-typed program can always step, and every step lands somewhere still well-typed, so it never gets stuck. That is the whole of it, and the word "wrong" in the slogan means precisely "stuck in this model" — nothing else.
Everything therefore depends on what the model contains. If the model has no exceptions, then a division by zero is stuck and a sound system must rule it out. If the model defines division by zero as raising an exception, then raising is a legitimate step, the program is not stuck, and soundness has nothing to say about it. This is not a loophole; it is what the theorem is for, and it is why the useful question about any soundness claim is "sound with respect to which model?"
PROGRESS If ⊢ e : τ then either e is a value,
or ∃e′. e → e′
PRESERVATION If ⊢ e : τ and e → e′
then ⊢ e′ : τ
COROLLARY A well-typed term never reaches a state that is
neither a value nor able to step — it never gets
"stuck". What counts as stuck is decided entirely
by which steps the model defines.Soundness is not "no bugs", and not "no runtime failures"
The most common overclaim in this area is to hear "sound type system" and understand "programs that compile are correct". A sound type system rules out the specific class of failure its model calls stuck. It says nothing about a program that computes the wrong answer with impeccable types, and nothing about anything the model does not describe.
What is routinely outside the model: logic errors of every kind; non-termination (a program that loops forever has not got stuck, it is stepping happily); resource exhaustion, since no model counts memory; anything reached through reflection, deserialization or foreign function interfaces, because those construct values without going through the typing rules; and, in most languages, arithmetic overflow, array bounds and division by zero, which are defined as exceptions or as wrapping behaviour so that they are steps rather than stuck states.
A sound language can therefore panic, throw, abort, deadlock and return nonsense, all while its soundness theorem holds. Rust is sound and Vec indexing out of range panics — the panic is a defined step. Haskell is sound and head [] throws. This is not a technicality: the class of error being excluded is "an operation was applied to a representation it was not defined for", and that class is genuinely worth excluding, because it is the one that corrupts memory and produces undefined behavior.
That is also the connection to the rest of this domain. Unsoundness is not merely aesthetic. When a value does not have the type the compiler recorded, every optimization that assumed the type is now transforming a program it has misunderstood, which is how a type hole becomes a miscompilation — see [[ub-and-optimization]].
Deliberate unsoundness, and what it was bought with
Several widely deployed type systems are unsound on purpose, and in every case the hole was traded for something specific. Treating these as mistakes misses the engineering.
Java's covariant arrays. String[] is a subtype of Object[], which means a String[] can be passed where an Object[] is expected and an Integer stored into it. That is statically type-correct and dynamically wrong, so the JVM inserts a runtime check on every array store and throws ArrayStoreException. Java bought a usable generic-free API for arrays in 1995 — before generics existed, there was no other way to write a method over any array — and pays for it with a check on every single array write, forever.
TypeScript's bivariant method parameters. Under strictFunctionTypes, function type parameters are checked contravariantly — correctly — except for parameters of methods declared with method syntax, which remain bivariant. So a Cat[] is assignable to an Animal[], and a handler taking Animal is interchangeable with one taking Cat. This was not an oversight; it was needed to keep the enormous body of existing JavaScript type declarations, including the DOM, compatible. TypeScript documents it as a known unsoundness.
TypeScript's `any`, casts and unchecked index access. Each is a documented hole with a stated motivation: migration, interoperability, and the fact that arr[i] returning T | undefined would have broken essentially every existing codebase. noUncheckedIndexedAccess exists precisely so that a project can close the last one and pay the cost itself.
Dart. Dart 1 had a deliberately unsound optional type system — annotations were largely documentation. Dart 2 replaced it with a static system that is sound *modulo* dynamic, and pays for it with runtime downcast checks: where the static side cannot prove a cast, the compiler inserts one that fails at runtime rather than letting a wrongly typed value proceed. That is the honest version of the trade — soundness restored by checking, at a cost you can measure.
The pattern across all four: the unsoundness buys compatibility with code that already exists, and is paid for either by an inserted runtime check or by an explicitly accepted gap. Both are legitimate. What is not legitimate is not knowing which one you have.
| Hole | What it permits | Bought | Paid with |
|---|---|---|---|
| Java covariant arraysspec | Storing an Integer into a String[] via Object[] | Generic-looking array APIs before generics existed | A runtime check on every array store; ArrayStoreException |
| TS bivariant method paramsimplementation | A handler for Cat used where one for Animal is required | Compatibility with existing JS/DOM type declarations | An accepted gap — no check is inserted, ever |
TS any and asimplementation | Any value at any type, in both directions | Incremental migration from untyped JavaScript | An accepted gap; see [[gradual-typing]] |
| TS unchecked index accessimplementation | arr[i] typed T when it may be undefined | Not breaking every existing codebase at once | An accepted gap, closable with noUncheckedIndexedAccess |
Dart 2 dynamicimplementation | A dynamically typed value flowing into typed code | Migration from Dart 1 and from untyped idioms | Inserted runtime downcast checks that can fail |
C++ reinterpret_castspec | Reading one representation as another | Systems programming that requires it | Undefined behavior — the compiler assumes it never happens |
The engineering position
null type and certain intersection cases) that survived for years. "This language is sound" always means "a model of a subset of it was proved sound, and the implementation aspires to match".The useful stance is not to sort languages into sound and unsound and prefer the first list. It is to know, for the system in front of you, where the holes are, whether each is checked at runtime or simply accepted, and therefore what you must do yourself at those points.
For an accepted gap — TypeScript's any, its bivariance, its index access — the compensating control is a runtime check at the boundary where untrusted values enter. That is the entire argument of [[gradual-typing]], arrived at from the soundness side.
For a checked hole — Java's array store, Dart's downcasts — the compensating control is knowing that the check exists, both because it costs something and because it can fail: an ArrayStoreException in production is a type error that was deferred rather than prevented, and it will appear at the write rather than at the mistake.
And there is a third category worth naming: systems that are sound in the language and unsound in the escape hatch. Rust is sound, and unsafe suspends the checking so that the invariants can be maintained by a human instead. The soundness claim then becomes conditional — the safe subset is sound *provided* every unsafe block upholds what it promised. That is a strictly better position than an unchecked hole, because the obligation is localised and greppable, and it is strictly worse than no hole at all, because the obligation is real. [[ownership-types]] is where that bargain is spelled out.
How it works
The steps, in the order the compiler takes them.
- A formal model is written down: a syntax, a typing judgement, and a small-step operational semantics defining which configurations can step and to what.
- Preservation is proved by induction on the typing derivation, showing each evaluation rule maps well-typed terms to well-typed terms at the same type.
- Progress is proved by induction on the typing derivation, showing that a well-typed term that is not a value always has an applicable rule — usually the case analysis where canonical-forms lemmas do the work.
- Where the language has a feature the model cannot make sound, the implementation has two options: insert a runtime check that turns the stuck state into a defined step (an exception), or document the gap.
- A compiler for a system with unchecked holes must therefore be careful which typing facts it feeds to the optimizer, since those facts may not hold of the actual values.
- An escape hatch such as
unsafeis modelled as a set of proof obligations transferred to the programmer: the safe fragment remains sound conditional on those obligations being met.
How it breaks
What the engineer observes when it goes wrong — not what goes wrong internally.
- An
ArrayStoreExceptionappears in production at a line that merely writes an element; the actual mistake was an upcast several call frames earlier, and the stack trace points at neither. - A TypeScript event handler typed for a narrower event is registered where a broader one is dispatched; nothing errors at compile time and a property read returns undefined at runtime, several layers into a framework.
- A value arrives from
JSON.parseat a declared type it does not have; every downstream operation type-checks and the failure appears as arithmetic on undefined, far from the boundary. - A soundness hole is exercised by an optimizer: code that assumed a field's declared type is transformed on that basis, and the resulting behaviour differs between optimization levels — the hardest class of bug to attribute.
- A team reads "sound type system" as "cannot fail at runtime", removes defensive checks at a service boundary, and the first malformed upstream payload takes the process down.
- An
unsafeblock upholds its invariant on the day it is written; a later refactor changes a caller, the invariant no longer holds, and the safe code around it is now unsound with nothing reporting it.
When it helps
- Reasoning about what a compiler may assume: soundness is what licenses an optimizer to trust a declared type without inserting a check.
- Evaluating a language or a type-checker honestly, by asking which holes exist and whether each is checked or accepted.
- Deciding where compensating runtime validation belongs — precisely at the boundaries where the model's assumptions stop holding.
- Understanding why a language inserts checks that look redundant: they are usually the price of a known hole.
When it hurts
- As a marketing property. "Sound" is a claim about a model, and a model can be small; the word alone tells you nothing about which failures the language excludes.
- When it drives a rewrite. Migrating to a sound language moves one class of failure and leaves logic errors, resource limits and boundary data exactly where they were.
- When pursued to the exclusion of adoptability. A sound gradual system pays a measurable performance cost at partially typed boundaries, which is a genuine reason a project might choose the hole.
- When it becomes an argument for removing runtime validation. The theorem covers the code the checker saw, and never the data.
What it costs
Every one of these is paid by something.
- Soundness buys the right for every later phase to trust the types, and pays by rejecting programs that are in fact fine — every sound system is conservative, and the rejected-but-correct programs are a real ergonomic cost paid daily.
- A deliberate hole buys compatibility with an existing ecosystem and pays either a permanent runtime check on a hot operation (Java's array store) or a permanent, unreportable gap (TypeScript's bivariance).
- Restoring soundness by inserting checks buys a real guarantee and pays in throughput and in a new failure mode: the check itself, which fires at the use rather than at the mistake.
- An
unsafe-style escape hatch buys expressiveness at the cost of making the soundness claim conditional and non-local — the obligation is on a human, is not checked, and survives only as long as nobody refactors around it.
What else you could do
What a different compiler or language does instead, and when that is better.
- Full dynamic typing gives up static soundness entirely and checks representations at every operation, which is a coherent design: nothing is ever stuck because every operation has a defined failure step.
- Sound gradual typing (Typed Racket) keeps the guarantee by inserting contracts at typed/untyped boundaries, and pays measurable overhead in exactly the partially typed configurations that motivated the design.
- Formal verification of the program rather than the type system — proofs about the actual code, not just its representations — covers the logic errors that soundness never addressed, at enormously higher cost. See
[[verified-compilers]]for the same trade applied to compilers themselves. - A sound core with an audited escape hatch (Rust) localises the obligation rather than removing it, which is the pragmatic middle and is why
unsafeblocks are conventionally small and commented with their invariant.
See it for yourself
The flag, dump or tool that shows you this directly.
- TypeScript:
tsc --strictFunctionTypesand then observe that method-syntax parameters remain bivariant — a two-file experiment demonstrates the hole in about a minute. tsc --noUncheckedIndexedAccesson any existing codebase shows how many array and record accesses were relying on that particular gap.- Java: write the four-line array covariance example and run it; the
ArrayStoreExceptionis the runtime check being visible.javap -con the method shows nothing — the check is in the JVM, not in the bytecode. - Dart: compile with
--sound-null-safetyand inspect the generated code for inserted downcast checks, which are the cost of restoring the guarantee. - For the theory itself, the reference implementations that accompany "Types and Programming Languages" let you step a well-typed term and watch preservation hold, which is more convincing than reading the proof.
Plausible wrong readings
Stated the way a confident engineer states them.
- "Sound means my program cannot crash." It means the model has no stuck states. Panics, exceptions and aborts are all defined steps, and every sound language has them.
- "An unsound type system is a broken type system." Several of the most widely used systems are unsound deliberately, in exchange for compatibility with code that already existed. The question is whether the hole is checked or accepted.
- "If it type-checks, the optimizer can trust it." Only if the system is sound with respect to a model that includes what the optimizer is assuming. That gap is where type holes turn into miscompilations.
- "Rust is sound, so
unsafeis fine as long as it compiles."unsafetransfers the obligation to you. The safe code around it is sound conditional on your having discharged it, and nothing checks that you did.
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 sound if programs it accepts never reach a state where an operation is applied to something it was not defined for — no adding a string to a function pointer, no reading memory as the wrong type. That is a narrow and valuable guarantee. It is not "no bugs": a sound program can compute the wrong answer, throw, loop forever, or run out of memory, all with its guarantee intact.
practical
For everyday work the useful question is where your language's holes are and how each is paid for. In TypeScript they are any, type assertions, method-parameter bivariance and unchecked index access — all accepted gaps with no runtime check, which is why validation at the data boundary is not optional. In Java the array-store hole is checked at runtime, so it costs you a check and an occasional exception rather than a silent wrong value. In Rust the hole is unsafe, which is a promise you made and nothing verifies. Knowing which category you are in tells you where your own defences go.
advanced
The deepest point is that soundness is a relationship between two artifacts you get to choose: the typing rules and the operational semantics. Make the semantics more permissive — define division by zero as an exception, define an out-of-bounds read as a panic — and previously stuck states become steps, so the system becomes sound without the type system doing anything new. That is not cheating; it is a real design lever, and it is exactly what C declines to pull. C leaves those cases undefined instead, which means the model says nothing, which in turn means the compiler may assume they do not happen, which is the entire mechanism behind [[ub-and-optimization]]. So the same lever that makes a language easy to prove sound is the one that decides whether a buffer overrun is a defined panic or a licence for the optimizer. Soundness, undefined behavior and optimization legality are three views of one decision about what the model admits.
How much this depends on
Nothing in this domain is true of every compiler. These say how much.
ArrayStoreException are specified in the JLS and the JVM specification: the check is mandatory, on every reference array store, and cannot be elided by a compiler unless it can prove the exact type. This is a language-level decision, not a HotSpot behaviour, and it is the reason List<T> is invariant while T[] is not.strictFunctionTypes is documented compiler behaviour with a stated compatibility motivation, and applies to method syntax but not to property-with-function-type syntax — so the same interface written two ways checks differently. This is TypeScript-specific and has no analogue in Flow or in a sound system.dynamic" reflects the Dart team's own framing: the static system is designed to be sound, and where the static side cannot discharge a cast, the compiler inserts a runtime check rather than allowing an ill-typed value through. Dart 1 made the opposite choice explicitly. Both are the same language name at different major versions, which is a reminder that soundness is a property of a version.If you were asked this in an interview
- State soundness precisely. What do progress and preservation each say, and what does "go wrong" mean?
- Java's arrays are covariant and this is unsound. What does the language do about it, and what does that cost?
- Name a deliberate unsoundness in a type system you use, say what it was traded for, and say what you do to compensate.