Tipos dependentes
Tipos que dependem de valores, permitindo expressar invariantes no próprio sistema de tipos: Vec n Int é um vetor de exatamente n inteiros, e o compilador confere o tamanho.
São o padrão em assistentes de prova como Coq, Agda e Lean. Fora da academia, os nomes de peso são Idris, F* (Microsoft Research) e o Lean 4. Casos de uso: software certificado (o compilador C CompCert), provas de criptografia e contratos inteligentes. A contrapartida: poder enorme, mas compilações que levam minutos e uma carga mental alta.
Linguagens OO mainstream não têm tipos dependentes; Rust, Java e Go ficam com genéricos limitados. O Lean 4 é ensinado em cursos de métodos formais no MIT e na CMU, e a Mathlib já formalizou a maior parte da matemática de graduação.