Il y a des tas de raisons de trouver que la théorie des types est un objet intéressant. C'est (dans certaines variantes) un langage de programmation dans lesquel il est impossible d'écrire un programme qui boucle mais le démontrer nécessite de travailler dans des systèmes inhabituellement forts.