Dependent types
Types die van waarden afhangen: invarianten worden onderdeel van het typesysteem, zodat Vec n Int een vector van precies n gehele getallen is en de compiler de lengte controleert.
Standaard in bewijsassistenten als Coq, Agda en Lean. Buiten die wereld zijn Idris, F* (Microsoft Research) en Lean 4 de bekendste voorbeelden. Toepassingen: gecertificeerde software (de C-compiler CompCert), bewijzen voor cryptografie en slimme contracten op blockchains. De afweging: enorm krachtig, maar compileertijden kunnen minuten duren en de mentale belasting is hoog. Gangbare talen als Rust, Java en Go hebben geen dependent types en moeten het doen met begrensde generics. Lean 4 wordt gedoceerd in formele-methodencursussen aan MIT en CMU, en Mathlib heeft het grootste deel van de wiskunde uit de eerste studiejaren geformaliseerd.