Posté par gasche .
En réponse à la dépêche OCaml 4.03.
Évalué à 3.
Dernière modification le 04 mai 2016 à 17:30.
Je trouve que les discussions sur LinuxFR sont souvent trop agressives, désagréables et peu accueillantes. Du coup ici j'essaie de faire des efforts pour qu'on ne tombe pas dans le "j'ai dit, tu as dit...", même si mon premier post dans la discussion n'était pas fameux en terme de convivialité—j'ai été un peu dur sur le fait que je trouvais l'utilisation de Rice fumeuse.
Je pense que quand tu as écrit
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 [..]
c'était une mauvaise formulation et tu avais sans doute quelque chose d'autre en tête. Par exemple maintenant tu écris
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.
Certes, le théorème de Rice est une exemple notable de résultat formel qui dit que raisonner sur les programmes est difficile. Mon problème avec le fait de l'utiliser dans ce cadre, c'est que tout le monde a l'habitude que quand on s'appuie sur un théorème, c'est pour faire une démonstration qui est formellement valide. Ta première formulation utilise les habits du raisonnement logique ("le théorème dit... donc..."), on pourrait croire que tu veux dire que le théorème de Rice prouve que "les mathématiques ne suffisent pas"—alors que tu as en tête (je suppose après notre discussion) une affirmation empirique sur l'état d'utilisabilité des outils de preuve de programme aujourd'hui.
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é.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par gasche . En réponse à la dépêche OCaml 4.03. Évalué à 3. Dernière modification le 04 mai 2016 à 17:30.
Je trouve que les discussions sur LinuxFR sont souvent trop agressives, désagréables et peu accueillantes. Du coup ici j'essaie de faire des efforts pour qu'on ne tombe pas dans le "j'ai dit, tu as dit...", même si mon premier post dans la discussion n'était pas fameux en terme de convivialité—j'ai été un peu dur sur le fait que je trouvais l'utilisation de Rice fumeuse.
Je pense que quand tu as écrit
c'était une mauvaise formulation et tu avais sans doute quelque chose d'autre en tête. Par exemple maintenant tu écris
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.
Certes, le théorème de Rice est une exemple notable de résultat formel qui dit que raisonner sur les programmes est difficile. Mon problème avec le fait de l'utiliser dans ce cadre, c'est que tout le monde a l'habitude que quand on s'appuie sur un théorème, c'est pour faire une démonstration qui est formellement valide. Ta première formulation utilise les habits du raisonnement logique ("le théorème dit... donc..."), on pourrait croire que tu veux dire que le théorème de Rice prouve que "les mathématiques ne suffisent pas"—alors que tu as en tête (je suppose après notre discussion) une affirmation empirique sur l'état d'utilisabilité des outils de preuve de programme aujourd'hui.
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é.