Types dépendants Dependent types
Des types qui dépendent de valeurs. Ils permettent d'exprimer des invariants dans le système de types : Vec n Int = un vecteur d'exactement n entiers, et le compilateur vérifie la cohérence des longueurs. Standard dans les assistants de preuve (Coq, Agda, Lean).
Du côté des langages utilisables en pratique : Idris, F* (Microsoft Research) et Lean 4, le plus moderne. Cas d'usage : logiciels certifiés (le compilateur C CompCert), preuves cryptographiques, contrats intelligents. Le compromis : une puissance énorme, mais des temps de compilation qui peuvent se compter en minutes et une charge mentale élevée. Les langages généralistes comme Java ou Go n'en ont pas ; Rust s'en approche de loin avec les const generics. Lean 4 est enseigné dans des cours de méthodes formelles, notamment au MIT et à CMU, et sa bibliothèque Mathlib a formalisé une bonne partie des mathématiques de premier cycle.