Type Systems: Static, Dynamic, Strong & Weak

A production static type checker is normally designed to terminate before the program runs, although type checking or inference is undecidable for some formal type systems. For a Turing-complete model, Rice's theorem rules out deciding every nontrivial extensional property of the partial function a program computes; it does not say that every question about source text or every bounded execution is undecidable. Decidable sound checkers therefore use rules that conservatively approximate selected semantic properties, while other systems deliberately trade soundness for acceptance or defer checks to run time. Almost every argument about types is really an argument about where those boundaries should sit, and most of the vocabulary used in those arguments — "strongly typed", "type-safe" — is used loosely enough to be useless.

The two axes that get conflated #

"Static vs dynamic" and "strong vs weak" are independent questions.

Static vs dynamic is when types are checked: at compile time against the program text, or at run time against the value in hand. Nearly every language does some of both — Java checks assignments statically and casts dynamically.
Strong vs weak is whether the check can be silently bypassed. A weakly typed language will reinterpret the bits of one type as another without complaint, either by implicit coercion or by unchecked memory reinterpretation.

	Weak	Strong
Static	C, C++ (a `void*` cast reinterprets memory; no runtime check)	Rust, Haskell, Java, Kotlin, Go
Dynamic	JavaScript (`[] + {}` is `"[object Object]"`), PHP	Python, Ruby, Clojure — wrong types raise, they do not coerce

Soundness, and the holes real languages keep on purpose #

A sound type system guarantees a well-typed program cannot commit the errors the system claims to prevent. Real languages trade soundness away when the alternative is too inconvenient, and the trades are worth knowing because they are the ones that bite.

Java and C# array covariance. String[] is a subtype of Object[], which is unsound: an Object[] reference can be written with an Integer.

java

String[] names = new String[1];
Object[] any   = names;        // compiles — arrays are covariant
any[0] = Integer.valueOf(42);  // compiles, throws ArrayStoreException at run time

The language pays for this with a store check on every array write to a reference array — a permanent runtime cost imposed on all correct code to catch a mistake the type system chose not to reject. Generics learned the lesson and are invariant (see generics and variance).

TypeScript is unsound by design. Its non-goal list says so explicitly: it aims to be a productive checker over idiomatic JavaScript rather than a proof system. Method parameters are compared bivariantly, any disables checking entirely, and — the one that matters operationally — types are erased at run time, so a value crossing an I/O boundary is whatever the network actually sent.

typescript

const user: User = await res.json();   // no check whatsoever happens here

This is the single most common source of "impossible" runtime errors in typed JavaScript codebases. The declared type is a comment; the runtime shape is data. See preconditions and boundaries — the fix is a parser at the edge, not a stronger annotation.

Nominal vs structural #

Whether A is a subtype of B can be decided by declared name or by shape.

	Nominal	Structural
Rule	subtyping only when declared (`implements`, `extends`)	subtyping when the members match
Languages	Java, C#, Rust, Kotlin	Go interfaces, TypeScript, OCaml objects
Wins at	intent — two types with identical shape but different meaning stay distinct	retrofitting — an interface can be declared after the concrete types exist, without touching them
Loses at	ceremony; adapters to bridge structurally-identical types	accidental conformance — a type satisfies an interface it was never meant to

Go's choice is the interesting one for design: because interfaces are structural and satisfied implicitly, the interface belongs to the consumer, not the producer. That inverts the usual dependency direction for free — the package that needs a Reader declares Reader, and nothing upstream knows. See interfaces and abstract types.

Inference is not dynamism #

var, auto, let, and := infer a type at compile time and then enforce it as usual. Hindley–Milner (Milner 1978) infers principal types for a whole program without annotations; most mainstream languages deliberately use only local inference instead, because whole-program inference produces error messages that point far away from the mistake and makes a function's public signature depend on its body.

That is why Rust, Kotlin, and Go all infer inside function bodies and require annotations on signatures: the signature is the contract, and a contract that is inferred can be changed accidentally by an unrelated edit to the implementation.

What it is measurably worth #

The honest empirical answer is narrower than either camp claims. Gao, Bird and Barr took 400 fixed bugs from public JavaScript projects, checked out the code before each fix, added type annotations, and asked whether a checker would have flagged it:

15% of the bugs were detectable by TypeScript 2.0 or Flow 0.30 (95% CI: 11.5%–18.5%).
The two tools were close to interchangeable in what they caught.

So types are not a substitute for tests — they catch roughly one bug in seven at the point of writing. The other value, which the study does not measure, is what the annotations do for refactoring, navigation, and API discoverability, and that is usually the reason teams adopt them.