Typy zależne
Typy, które zależą od wartości — pozwalają zapisać niezmienniki w systemie typów, np. Vec n Int to wektor dokładnie n liczb całkowitych, a kompilator pilnuje zgodności długości.
Standard w asystentach dowodzenia (Coq, Agda, Lean). Poza nimi: Idris, F* (Microsoft Research) i nowoczesny Lean 4. Zastosowania to certyfikowane oprogramowanie (kompilator C CompCert), dowody w kryptografii i inteligentne kontrakty. Cena: ogromna siła wyrazu, ale kompilacja potrafi trwać minuty, a obciążenie umysłowe jest wysokie. Głównonurtowe języki obiektowe typów zależnych nie mają — Rust, Java i Go poprzestają na ograniczonych generykach. Lean 4 uczy się na kursach metod formalnych na MIT i CMU, a Mathlib, biblioteka matematyczna Leana, zformalizowała większość matematyki licencjackiej.