Plein de cas courant peuvent être résulu, et c'est cela qui nous permet d'écrire des prouveurs, ou de faire marcher des algos de model-checking.
Il n'empeche que même dans les cas courant (de l'industrie) il y a des cas emmerdant qui ne fonctionnent pas avec les techniques actuels. Que cela soit avec le prouveur de B ou n'importe quel autre. La principale limite étant que la complexité de ce genre d'algo est généralement exponentielle. Alors qu'un être humain arrive, plus ou moins, a *voir* la solution directement.
En pratique en B on dirige le prouveur en lui faisant faire des cas intermédiaire et en lui machant le travail. Alors même dans les preuve à la main le prouveur est essentiel.
Perso je trouve que ca marche pas trop mal, bon ok defois on s'arrache les cheveux et sa demande pas mal d'expérience et de temps.
[^] # Re: qques questions sur Lissac et... Ruby, Java, Caml...
Posté par Joris R (site web personnel, Mastodon) . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 1.
Plein de cas courant peuvent être résulu, et c'est cela qui nous permet d'écrire des prouveurs, ou de faire marcher des algos de model-checking.
Il n'empeche que même dans les cas courant (de l'industrie) il y a des cas emmerdant qui ne fonctionnent pas avec les techniques actuels. Que cela soit avec le prouveur de B ou n'importe quel autre. La principale limite étant que la complexité de ce genre d'algo est généralement exponentielle. Alors qu'un être humain arrive, plus ou moins, a *voir* la solution directement.
En pratique en B on dirige le prouveur en lui faisant faire des cas intermédiaire et en lui machant le travail. Alors même dans les preuve à la main le prouveur est essentiel.
Perso je trouve que ca marche pas trop mal, bon ok defois on s'arrache les cheveux et sa demande pas mal d'expérience et de temps.