Posté par gasche .
En réponse à la dépêche OCaml 4.03.
Évalué à 5.
Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes : et donc là on se tourne vers des méthodes scientifiques, Popper et les tests. Donc oui, quand on peut faire des maths c’est mieux, mais en pratique c'est malheureusement pas possible.
Le théorème de Rice nous dit qu'un ordinateur ne peut pas décider automatiquement des propriétés non triviales. Ça n'empêche en rien de les prouver avec des mathématiques, ou d'apporter à l'ordinateur des informations supplémentaires (par exemple: une dérivation dans un système de type fixé, ou des invariants et préconditions, etc.) qui rendent le problème décidable.
Le passage de Rice à "les mathématiques ne sont pas possibles" est à mon avis un bel exemple d'extension abusive d'un résultat scientifique, comme on en lit souvent sur le théorème de Gödel ou sur la physique quantique. Je ne suis pas trop sûr de vers où part cette discussion.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par gasche . En réponse à la dépêche OCaml 4.03. Évalué à 5.
Le théorème de Rice nous dit qu'un ordinateur ne peut pas décider automatiquement des propriétés non triviales. Ça n'empêche en rien de les prouver avec des mathématiques, ou d'apporter à l'ordinateur des informations supplémentaires (par exemple: une dérivation dans un système de type fixé, ou des invariants et préconditions, etc.) qui rendent le problème décidable.
Le passage de Rice à "les mathématiques ne sont pas possibles" est à mon avis un bel exemple d'extension abusive d'un résultat scientifique, comme on en lit souvent sur le théorème de Gödel ou sur la physique quantique. Je ne suis pas trop sûr de vers où part cette discussion.