Oui, enfin rappelons avec monsieur Gödel que la preuve se base forcément sur quelque-chose de « plus fort » que la théorie de Coq elle-même. Il n'y a pas de preuve de cohérence de Coq en Coq, sans ajouter d'axiome supplémentaire, et (autre façon de voir les choses) il est impossible pour la même raison de coder l'algorithme de réduction du calcul des constructions inductives, la base formelle de Coq, en Coq.
Pour reprendre une image de Jean-Yves Girard, les preuves de cohérences sont des assurances contre l'explosion de la Terre (même si elle peuvent avoir des retombées pratiques et nous apprendre des choses).
[^] # Re: Se passer des tests ...
Posté par auve . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
Pour reprendre une image de Jean-Yves Girard, les preuves de cohérences sont des assurances contre l'explosion de la Terre (même si elle peuvent avoir des retombées pratiques et nous apprendre des choses).