Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable. Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.
et je suis complètement d'accord avec ça. J'espère qu'on est tous les deux d'accord sur le fait que ça n'a pas grand chose à voir avec le théorème de Rice.
Ben si, car comme je le disais :
Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif.
Ainsi de nombreuses propriétés intéressantes ne peuvent pas être prouvée par un compilateur. Alors, oui, certes, sur un programme particulier tu peux faire la démonstration toi même, mais en pratique ça devient vraiment trop lourd. Sans être direct, le lien existe bien. La conséquence concrète de Rice c'est qu'on doit se farcir le boulot (en partie) à la main ; c’est très concret comme résultat.
Alors certes on pourrait imaginer un outil qui nous aiderai tellement que la partie à faire à la main serait super facile, mais un tel outil n'existe pas. De même que l'on pourrait imaginer des programmes qui permettent de résoudre concrètement des problèmes non polynomiaux car de complexité en o( 10-9999...9999 2n ).
Se poser la question des conséquences concrètes d'un théorème mathématique est toujours délicat car à notre échelle notre monde n'est pas mathématiques. Même des programmes prouvés formellement peuvent avoir des bugs car ils tournent sur des machines imparfaites. Mais il ne faut pas non plus être trop rigide et accepter quelque imprécision quand on cherche à interpréter concrètement les grands théorèmes.
Je trouve qu'invoquer Popper et Rice à tour de bras ça fait un peu snob; quand c'est bien employé, pourquoi pas, mais je réagis vite quand c'est mal employé.
Ben je n'ai pas l'impression que Rice constitue un lieu commun comme Gödel ou la physique quantique. Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque... Pas plus que d'invoquer Popper pour dire prendre un peu de recul et de constater que les tests unitaires ne sont en fait simplement qu’une application des principes des sciences expérimentales à l'informatique.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par Diagonale de Cantor (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 4.
Ben si, car comme je le disais :
Ainsi de nombreuses propriétés intéressantes ne peuvent pas être prouvée par un compilateur. Alors, oui, certes, sur un programme particulier tu peux faire la démonstration toi même, mais en pratique ça devient vraiment trop lourd. Sans être direct, le lien existe bien. La conséquence concrète de Rice c'est qu'on doit se farcir le boulot (en partie) à la main ; c’est très concret comme résultat.
Alors certes on pourrait imaginer un outil qui nous aiderai tellement que la partie à faire à la main serait super facile, mais un tel outil n'existe pas. De même que l'on pourrait imaginer des programmes qui permettent de résoudre concrètement des problèmes non polynomiaux car de complexité en o( 10-9999...9999 2n ).
Se poser la question des conséquences concrètes d'un théorème mathématique est toujours délicat car à notre échelle notre monde n'est pas mathématiques. Même des programmes prouvés formellement peuvent avoir des bugs car ils tournent sur des machines imparfaites. Mais il ne faut pas non plus être trop rigide et accepter quelque imprécision quand on cherche à interpréter concrètement les grands théorèmes.
Ben je n'ai pas l'impression que Rice constitue un lieu commun comme Gödel ou la physique quantique. Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque... Pas plus que d'invoquer Popper pour dire prendre un peu de recul et de constater que les tests unitaires ne sont en fait simplement qu’une application des principes des sciences expérimentales à l'informatique.