Types as guarantees
Making the likeliest mistake in a system impossible to express, rather than merely against the rules.
There is a hierarchy of ways to prevent a defect, and most software sits at the bottom of it. The bottom is a convention someone is expected to follow. Above that is a check that runs and complains. At the top is a design in which the mistake cannot be written down at all, because there is nowhere to put it. We spend our effort moving rules upward through that hierarchy.
The distinction matters because conventions decay. A rule that lives in a code review comment survives exactly as long as the person who remembers it, and the failure mode is silent: nobody announces that a convention has been forgotten. A rule encoded in the structure of the code is enforced by a machine that does not get tired, does not need onboarding, and does not assume the previous author had a reason.
The most direct application is the absent field. Where a value must never be invented, the type carries no property for it. A component built to display a professional credential can be given a credential name and an issuing body and nothing else — there is no property for a registration number, so a fabricated registration number cannot be rendered, and adding one requires changing the type, which is a visible decision, not an accident during a busy afternoon.
The same technique applies to required values. Where a field must exist, it has no default. Defaults are convenient and they are how a required thing silently becomes optional: someone adds an entry, forgets the field, and gets a placeholder instead of an error. A required value that nobody supplied stops the work before it ships, which is the correct time to find out.
Union types replace stringly-typed identifiers. A status that can be one of five values is declared as those five values, not as text, so a mistyped status is refused outright instead of becoming a record that silently matches nothing. This one change eliminates an entire class of bug that is otherwise found in production by a report that comes back empty.
Exhaustiveness checks make new cases visible. Where the code branches on a union, a totality check asserts every case is handled, so adding a sixth status causes every place that must now consider it to fail compilation. Without that, adding a case means finding the branches by memory, and the ones that are missed behave as though the new case does not exist.
Identifiers are given distinct types even when they are all strings underneath. A customer identifier and an order identifier are not interchangeable, and treating them as the same kind of thing means one will eventually be accepted where the other belongs. Distinguishing them costs a few lines and prevents a category of bug that is genuinely difficult to find by reading.
Data crossing a boundary is validated once, at the boundary, and typed thereafter. Anything arriving from a network request, a form, another company's system, or a file is untrusted until it has been checked, and after it has been checked it is a known shape that the rest of the system can rely on without re-checking. Validation scattered through the interior is a sign the boundary was never established.
Derived values are computed rather than stored alongside their inputs. A total that is stored next to the line items it sums is two facts that can disagree, and eventually will. Where a value must be stored for performance or for historical accuracy, that is a deliberate decision with a note explaining why, not a default.
The technique has limits and we state them. A type system cannot verify that a number is the right number, that a business rule matches what the business intends, or that a fact is true. It moves a specific class of mistake — the structural, the forgotten, the mistyped — from the moment a customer meets it to the moment it is written. Everything outside that class still needs tests, review, and judgment.
There is also a cost in expressiveness. Strict types make some quick things slower to write, and there is a point past which additional strictness produces more ceremony than safety. The judgment is about which mistakes this particular system is most likely to make, and pushing those up the hierarchy instead of pushing everything up uniformly.
Typecheck runs as its own step, not only as part of the build, and it runs in verification before anything is deployed. Tooling that discards these rules without applying them will happily produce output from work that never satisfied them, which turns a guarantee back into a surprise.
Configuration gets the same treatment as code. Where a system is driven by a settings file — a list of services, a set of regions, a schedule — that file is typed against the shape the code expects, so an entry with a missing field or a misspelled name is refused outright instead of producing a page that silently renders nothing. Configuration is where this class of error is most common, because it looks like data and is therefore assumed to be harmless.
The payoff arrives when someone unfamiliar changes the system. A person who has never seen the code, working from a ticket, guided by a system that refuses the wrong shapes, will produce a change that is structurally correct on the first attempt. That is the actual value of the technique: it transfers knowledge from the person who left to the person who arrived, without either of them meeting.
The test of whether this is working is not the absence of type errors. It is whether, when someone makes the mistake the system is most prone to, something stops them before a customer does.
What this does not cover.
- Suppressing type errors to unblock a build. An error suppressed is a guarantee withdrawn.
- Checking values as they pass by, used as a substitute for a real boundary. Data is checked where it enters, not repeatedly in the interior.
- Type-level programming whose complexity exceeds the defect it prevents.
Software Engineering
Specification before code
The document that names every entity, every state, and every failure path — and why a project that cannot produce it should not start.
Internal tools
Authenticated back-office systems for the work currently living in a spreadsheet.
Commerce and payments
Checkout, registration, and subscription flows built against the client's own payment account.
Moving data between systems
Reversible where possible, rehearsed against a copy, and always producing a record of what changed.
Interfaces between systems
The interfaces a system exposes, and the contracts it holds itself to once something depends on them.
Testing
Coverage aimed at what would actually be expensive to get wrong, instead of at a percentage.