Tipos dependientes
Tipos que dependen de valores. Permiten expresar invariantes en el propio sistema de tipos: Vec n Int es un vector de exactamente n enteros, y el compilador verifica la consistencia de la longitud. Estándar en asistentes de demostración (Coq, Agda, Lean).
Relevancia fuera del mundo académico: Idris, F* (Microsoft Research), Lean 4. Erlang/Elixir tiene "specs" como una versión débil del concepto. Casos de uso: software certificado (el compilador de C CompCert), pruebas criptográficas, contratos inteligentes. La contrapartida: son enormemente potentes, pero los tiempos de compilación pueden llegar a minutos y la carga mental es alta. Los lenguajes OOP mainstream no tienen tipos dependientes — Rust, Java y Go se quedan en "value restriction" y genéricos acotados. Lean 4 se enseña en cursos de métodos formales del MIT y CMU; Mathlib, su biblioteca matemática, ha formalizado buena parte de las matemáticas de grado.