Dans cet exposé, nous rentrerons dans les coulisses d'un assistant de preuve basé sur la théorie des types. Nous nous focaliserons en particulier sur les contraintes techniques résultant de ce choix de fondation, notamment au niveau de l'importance du calcul au sens large. Contrairement à l'image austère et surranée que pourrait semondre ce genre de thématique, il s'agit en fait d'un sujet bouillonant aux nombreuses conséquences aussi bien en termes de design que pour l'usage d'un tel logiciel.