type-driven
Type-driven development
Types encode the specification -- design from requirements before implementation. Make illegal states unrepresentable (Yaron Minsky). Parse, don't validate (Alexis King). For parsed opaque domain types within trusted boundaries, if the type compiles, the value is valid.
Modern insight (2025): "Encode invariants in types, not runtime checks" is the evolved formulation. Type richness should match risk -- start simple, add complexity where bugs actually occur. Types serve AI-assisted development: they communicate intent better than comments and reduce LLM hallucinations.
See patterns for language-specific refined types, state machine techniques, and language-specific validation gates. See examples for brief "parse, don't validate" patterns per language. See formal-tools for dependent type systems and verification tools.
Parse, Don't Validate
- Validate: Check if data is valid -> return bool -> caller must remember check happened. Proof is lost.
- Parse: Transform untrusted data into typed value that proves validity -> return new type. Proof is preserved.
- Consequence: Once parsed into an opaque domain type, internal code within trusted boundaries receives typed values and should not re-validate the same invariant. Note: deserialization, casts, FFI, and unsafe escape hatches can bypass the type system -- runtime checks remain necessary at those boundaries.
- Alexis King clarification: Newtypes are convenient but encapsulation-dependent. Best for simple invariants. Phantom types and branded types provide richer guarantees.