• [^] # Re: prouveur automatique/assistant de preuve

    Posté par (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.

    1) on n'observe pas les contre-exemple

    Un contre-exemple est un exemple qui contredit une hypothèse. Par conséquent, si j'émet l'hypothèse "tous les cygnes sont blancs", et que je croise un cygne noir, j'observe un contre-exemple.

    2) on ne prouve pas les cygnes.

    Et c'est pour ça que j'ai parlé de prouver la théorie "tous les cygnes sont blancs". On prouve (enfin, on conforte) des théories.

    Ensuite, naturellement, Dijkstra est toujours pertinent, et ici si on veut se ramené à nos histoires de sciences expérimentales, avec les tests de programmes on teste l'hypothèse "ce programme n'a pas de bugs". Les tests peuvent la réfuter, mais jamais la prouver.