Il me semble que pour Coq, il ont essayé de réduire au maximum l'ensemble représentant les axiomes de base afin de les prouver "à la main", et de faire prouver le reste de Coq à partir de ça. Bon, c'est assez approximatif, si quelqu'un avait une explication plus clair, je suis pour.
[^] # Re: Se passer des tests ...
Posté par benoar . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 4.