Je ne suis pas d'accord avec ton approche «Ce que l'homme est capable de faire, et que l'ordinateur ne peut pas faire». À 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.
Ok, on a pas encore de machine capable de faire ça, mais à ne pas en douter, ça va venir. C'est même le genre de réflexion qui terrifie [[Bill Joy]] (et paf le cheminl'argument d'autorité).
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 ? 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 ? Dans le pire des cas, le cas rare ce produira et le malchanceux fera un rapport de bogue. La majorité des logiciels ne sont pas destinés à lancer des fusés ou guider des avions hein.
Cela dit, je comprends bien l'aspect branlette intellectuelle, la satisfaction que ce serait de ce dire que son logiciel est «parfait», qu'il tourne tip-top sur son OS micro-noyau écrit en ADA. Mais bon avoir un OS à noyau monolithique qui répond bien à mes besoins concrets, c'est déjà pas si mal.
[^] # Re: prouveur automatique/assistant de preuve
Posté par psychoslave__ (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
Ok, on a pas encore de machine capable de faire ça, mais à ne pas en douter, ça va venir. C'est même le genre de réflexion qui terrifie [[Bill Joy]] (et paf le cheminl'argument d'autorité).
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 ? 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 ? Dans le pire des cas, le cas rare ce produira et le malchanceux fera un rapport de bogue. La majorité des logiciels ne sont pas destinés à lancer des fusés ou guider des avions hein.
Cela dit, je comprends bien l'aspect branlette intellectuelle, la satisfaction que ce serait de ce dire que son logiciel est «parfait», qu'il tourne tip-top sur son OS micro-noyau écrit en ADA. Mais bon avoir un OS à noyau monolithique qui répond bien à mes besoins concrets, c'est déjà pas si mal.