Saying that one type is a subtype of another asserts that its values behave acceptably anywhere the supertype is expected — not merely that the members line up. Which real languages and tools actually try to check that behavioural assertion mechanically, how far does each one get, and what do teams do on a stack where nothing checks it at all?

## What the declaration actually promises When you declare that `B` is a subtype of `A`, callers become entitled to hold a `B` through an `A`-shaped reference and get `A`-shaped behaviour: the operations return what `A` promised, leave the state `A` promised, and refuse what `A` said they would never do. That is a claim about *observable behaviour over time*. What a type checker verifies is far weaker — that members with compatible signatures exist — and then it trusts you. Everything between "the signatures line up" and "the object actually behaves like one" is unverified; the design discipline that fills the gap is the Liskov Substitution Principle, covered on its own. The interesting question is how far real systems get toward mechanising the check, and what you do at the many points where they get nowhere. ## Level 0 — structural systems assert the claim *for* you In Go, a type satisfies an interface simply by having methods with the right names and signatures; there is no `implements` and no declaration anywhere. In TypeScript the same is true of object types. The consequence is that a subtype claim can come into existence without any human ever making one. The canonical Go case: you add `String() string` to a type as a debugging helper, and it now satisfies `fmt.Stringer`, so every `%v` in the program routes through it — and if that method formats its own receiver with `%v` it recurses until the process dies. Adding `Error() string` silently makes a type an `error`. TypeScript has the mirror problem: any object literal with a matching shape is accepted where your carefully-named domain type was expected, however unrelated its meaning. Both languages have escapes that restore a *deliberate* claim: Go's sealed-interface trick (an unexported method in the interface, so only your package can satisfy it) and TypeScript's branding (a private field or a `unique symbol` property nobody outside can produce). Nominal systems — Java, C#, Kotlin, Rust — at least require a human to write the claim down, which is a social check, not a behavioural one. ## Level 1 — accept the claim, repair it at run time Java and C# both made arrays covariant: a `String[]` is usable as an `Object[]`. That is fine for reads and false for writes, and both languages knew it. Their answer was not to reject the claim but to police it: every array store carries a runtime type check, and a bad store throws `ArrayStoreException` in Java or `ArrayTypeMismatchException` in .NET. This is the clearest specimen of a type system knowingly accepting a behavioural claim it cannot honour and buying the difference back with a dynamic check. The motive was expressiveness before generics existed — you needed *some* way to write a routine over any array. The cost is a check on a very hot operation (which JITs then work hard to elide) and an error class that only fires when the offending write executes. ## Level 2 — systems that genuinely attempt the proof Ada 2012 lets a tagged type carry class-wide contracts, and **SPARK** discharges the resulting obligations *by proof at build time*: the prover reasons about every dispatching call, not only the ones a test happens to reach. **JML** with **OpenJML** does the same for Java — specifications are inherited by subclasses and the tool generates verification conditions asserting that each override still satisfies what it inherited. These are real mechanised checks of a behavioural claim, and their limits are equally real: they verify only what you wrote in the specification language, only over the language subset the prover supports, and they cost specification effort that most teams will not spend outside avionics, rail, or crypto. ## Level 3 — the language admitting it cannot check Rust encodes the limit in its grammar. `Send` and `Sync` are *unsafe* traits: the compiler auto-derives them structurally when every field already has them, and it propagates them through generic bounds — but it never verifies the semantic property that a value is genuinely safe to move to, or share with, another thread. When you need to claim one for a type built from raw pointers, you write `unsafe impl Send for MyType {}`, and the `unsafe` keyword *is* the admission: a behavioural obligation exists here that no compiler can discharge, so a human signs for it. Safe traits carry documented obligations too — an `Ord` implementation that is not a total order makes sorting produce nonsense or panic — but violating those is merely wrong, not undefined, so no keyword guards them. ## What you do when nothing checks it On a mainstream stack the honest answer is: mechanise it in tests, not in types. Write one *conformance suite* per supertype — the behavioural laws stated as executable tests over a factory — and run it against every implementer, including decorators and mocks; this is what a TCK is. Property-based testing raises the coverage of that suite from examples to generated inputs. External checkers (pluggable qualifier systems such as the Checker Framework) bolt on properties the language never had. And you narrow the promise itself: an interface that promises less has less to break. ## Interview shape One sentence that the type checker verifies shape and nothing else. Then the spread: Go and TypeScript infer the claim from a shape nobody declared; Java and C# accept covariant arrays and repair them on every store; SPARK and OpenJML actually prove inherited contracts at build time, at a specification cost; Rust's `unsafe impl` names the unverifiable obligation out loud. Close on the shared conformance suite as what you run where none of that exists.