Une preuve formelle permet justement de ne pas avoir besoin de ça.
Une preuve formelle te donne juste un résultat binaire. Oui la démonstration est juste ou bien Non y'a une merde.
Elle ne t'explique pas l'idée clé. Elle ne te fait pas comprendre intuitivement pourquoi la démonstration fonctionne.
Ensuite, si tu veux faire référence à un résultat qui existe déjà, c'est facile d'imaginer des libraries pour ça
Bien entendu. C'est pourquoi j'avais fait référence au boulot de Voevodsky (voir ici). Mais encore une fois cela ne communique pas l'idée de la démonstration.
[^] # Re: Math
Posté par patrick_g (site web personnel) . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 4.
Une preuve formelle te donne juste un résultat binaire. Oui la démonstration est juste ou bien Non y'a une merde.
Elle ne t'explique pas l'idée clé. Elle ne te fait pas comprendre intuitivement pourquoi la démonstration fonctionne.
Bien entendu. C'est pourquoi j'avais fait référence au boulot de Voevodsky (voir ici). Mais encore une fois cela ne communique pas l'idée de la démonstration.