Bon, sinon, je vois plusieurs réflexions sur le fait que la preuve d'un programme ne peut être fait de manière générale, et alors ? Du moment qu'elle le fait au moins aussi bien que le ferait un humain et en plus rapide, ça vaut le coups non ?
En pratique ce n'est pas le cas, on passe beaucoup de temps à s'arracher les cheveux pour comprendre pourquoi le prouveur automatique n'ai pas capable de faire ce truc qui a l'air trivial...
Après oui effectivement il y a des techniques «pousse-bouton» qui ne font que chercher a trouver des bug sans chercher l'exhaustivité et cela peut faire gagner pas mal de temps. Mais cela nécessite quand même d'écrire une spécification formelle et c'est souvent la dessus que les gens ont du mal.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Joris R (site web personnel, Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
En pratique ce n'est pas le cas, on passe beaucoup de temps à s'arracher les cheveux pour comprendre pourquoi le prouveur automatique n'ai pas capable de faire ce truc qui a l'air trivial...
Après oui effectivement il y a des techniques «pousse-bouton» qui ne font que chercher a trouver des bug sans chercher l'exhaustivité et cela peut faire gagner pas mal de temps. Mais cela nécessite quand même d'écrire une spécification formelle et c'est souvent la dessus que les gens ont du mal.