Je suis très surpris d'apprendre que Coq aurait été vérifié par Villani (je pense que ce n'est pas possible vu son domaine de travail et l'état de la formalisation mécanisée en analyse et en probabilités), je pense que tu as mal compris—mais je n'ai pas accès au livre pour vérifier. Le calcul formel est évidemment utilisé, mais il ne s'agit pas de la même chose (il s'agit d'une aide au calcul, pas d'une vérification des preuves elles-mêmes).
[^] # Re: Math
Posté par gasche . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 2.
Je suis très surpris d'apprendre que Coq aurait été vérifié par Villani (je pense que ce n'est pas possible vu son domaine de travail et l'état de la formalisation mécanisée en analyse et en probabilités), je pense que tu as mal compris—mais je n'ai pas accès au livre pour vérifier. Le calcul formel est évidemment utilisé, mais il ne s'agit pas de la même chose (il s'agit d'une aide au calcul, pas d'une vérification des preuves elles-mêmes).