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

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

    À partir du moment où je reproduit le shéma neuronale d'un cerveau humain dans un logiciel, je ne vois pas ce qui ferait que l'un soit incapable de faire virtuellement ce que l'autre fait physiquement.

    On ne sait pas ce qu'est la conscience humaine. Si c'est seulement une propriété émergente de l'agencement des atomes du cerveau, alors je suis d'accord, mais il y a des gens sérieux qui contestent ça, par exemple Penrose.

    Qu'est-ce qu'on en à faire que notre programme ne réponds pas au contrat dans des cas ultra rares auquel on aurait pas pensé soit même ?

    Tu supposes que dans tous les cas utiles/pratiques on peut prouver des choses (manuellement ou automatiquement). Ça reste à voir.

    Après, réfléchir à ce qu'on peut prouver et ce qu'on ne peut pas prouver, ce n'est pas de la branlette intellectuelle, et ça ne sert pas seulement à dire "je ne peux pas, donc je n'essaye pas". Ça sert aussi à savoir quelles sont les choses auxquelles je dois renoncer si je veux avoir une preuve solide.