David Hilbert a écrit :
Joe Cool <zierouhli@free.fr> writes:
Ce qui montre bien que vous n'avez rien compris. Qu'espérez-vous,
une preuve de la cohérence de coc dans coc? Vous atteignez les
sommets du ridicule.
Non j'espérais que l'arrogance naturelle de Joe Cool le ferait se précipiter dans le (gros-énorme) piège. Et il est tombé dedans comme un seul homme. Évidemment qu'on ne peut pas prouver la cohérence de Coq dans Coq. N'importe quel idiot sait cela.
Il faut en effet être idiot pour «savoir» cela. Le jour où quelqu'un
prouvera la cohérence de coc en coc, vous cumulerez des mandats: idiot
et ridicule.
Même le noyau Coq écrit en CaML n'est pas vérifié, pas davantage le
compilateur CaML, sans parler du matériel informatique. Cela fait un
gros paquet de choses à croire. Qui parlait de croyance ?
Je suppose que les mathématiciens sont vérifiés... C'est pas beau de se
mettre au dessus de son propre discours.
Et tout cela pour quoi ? Pour redémontrer des théorèmes de mathématiques totalement évidents, ou financer des projets où la créativité mathématique est NULLE. Et pourtant, ça se permet de
donner des leçons.
Au moins les logiciens servent à quelque chose. Il servent par exemple Ã
apporter un peu de sérieux en mathématiques, un peu de rigueur.
--
Joe Cool
