Instead of re-validating in every mutator, some languages let you make the invalid state impossible to construct: Rust's NonZeroU32, Ada's `subtype Percent is Integer range 0 .. 100`, an OCaml abstract type with a smart constructor, or a TypeScript branded type. Compare where each of those actually enforces the constraint, and what each one costs.

## The move: from repeated checks to one proof Routing all mutation through invariant-preserving methods still leaves the predicate as a runtime obligation you re-discharge at each entry point. The stronger move is to make the illegal state unconstructible, so the check happens once at the point where an untrusted value enters and every function downstream expresses its requirement in its signature rather than in a guard. The languages differ sharply in *where the enforcement lives* — construction, assignment, the type system, or nowhere — and each location has a distinct cost. ## Rust: check once, and the compiler cashes the invariant in `NonZeroU32` wraps a `u32` that is guaranteed non-zero. The only safe way in is `NonZeroU32::new(x)`, which returns `Option<NonZeroU32>`; once you hold the value, no further check exists anywhere. Two consequences are worth naming. First, the invariant becomes a *representation* fact: because zero is now an impossible bit pattern, the compiler uses it as a niche for the `None` case, making `Option<NonZeroU32>` exactly as large as a `u32`. `NonNull<T>` does the same for pointers, which is why `Option<Box<T>>` is pointer-sized. An invariant expressed in the type has bought a layout optimisation — something a runtime guard can never do. Second, the escape hatch changes the *category* of the bug. `NonZeroU32::new_unchecked` is `unsafe`: violating the invariant there is not a wrong answer, it is undefined behaviour, because other code has already been compiled on the assumption. Encoding an invariant into a type makes it stronger and makes its violation worse. The same technique generalises with the newtype pattern: a struct with a private field plus a validating constructor. The type system guarantees no other construction path exists because a private field cannot be set from outside the module. ## Ada: enforcement at every assignment `subtype Percent is Integer range 0 .. 100` and `Dynamic_Predicate` place the check on every assignment, parameter pass and return. This is the opposite trade from Rust: you pay repeatedly, and in exchange the constraint holds no matter how the value was produced — there is no unchecked constructor to misuse. In the high-assurance domains Ada targets, that uniformity is the product. It also composes with Ada's `Type_Invariant` on private types, which is checked at the package boundary instead, so one language offers per-store and per-boundary granularity side by side and asks the designer to choose. ## ML-family: the constructor is the only door, by typing In OCaml, a `.mli` may declare `type email` abstractly and export `val of_string : string -> email option`. Clients cannot build an `email` any other way, cannot destructure one, and cannot forge one with a cast. There is no runtime mechanism at all after construction — the guarantee is that *no code exists* that could produce an invalid value, which is checked statically. F# expresses the same with a single-case union whose constructor is private; Haskell with a module that exports the type but not its data constructor, plus `NonEmpty` for the commonest structural case. The cost is real and should be stated: every construction site must handle the failure case, so the option or result threads through the parsing layer; and clients lose pattern matching, so the module must export enough accessors to be usable, which is a design burden on the API author. ## TypeScript and Python: documentation wearing a type's clothes A TypeScript branded type is `type Email = string & { readonly __brand: unique symbol }`, produced by a function that validates and casts. Inside the type checker it behaves like a distinct type. At runtime it is a string, because the brand is erased by the compiler — there is no field, nothing to check, and `x as Email` bypasses the constructor with no runtime cost or consequence. Python's `NewType` is the same story with the type checker outside the runtime entirely. That is not useless — it stops honest mistakes and documents intent — but it dictates the placement rule: **anything crossing an I/O boundary must still be validated by executing code**. A value from `JSON.parse`, a request body, a row from a database written by another service, arrives as `any` and can be asserted into a branded type without ever passing the validator. Contrast JavaScript's `#`-field brand check, which is a genuine runtime test precisely because the field really exists. ## Choosing Ask two questions. *Where does untrusted data enter?* — put the single check there, and make the value's type change as it crosses, so no downstream function has to trust or re-check. *What does a violation cost?* — if it is a wrong answer, a validated newtype or an abstract type is enough; if it corrupts memory or unlocks a resource, prefer the language that re-checks on every store, or forbid the unchecked constructor by policy. And know what you give up. Types that carry proofs make some legitimate operations awkward: a builder that must pass through intermediate invalid states, deserialisation frameworks that construct by reflection and bypass your constructor entirely, and ORMs that materialise objects field by field. Those bypass paths are where invariants encoded in types most often leak, and they are worth naming before someone finds them in production.