Posté par gasche .
En réponse à la dépêche OCaml 4.03.
Évalué à 3.
On arrive déjà à prouver corrects des programmes non-triviaux aujourd'hui : des compilateurs, des micro-noyaux, des machines virtuelles, des algorithmes concurrents et distribués, des noyaux de navigateur web, et j'en passe. On ne fait pas de la vérification "tout automatique" (qu'est-ce que ce ça veut dire ?), on définit des spécifications et on essaie d'automatiser au maximum la vérification que l'implémentation lui correspond. Le théorème de Rice ne dit rien sur ce qui se passe dans ce cadre, et ça ne semble pas impossible en pratique puisqu'on y arrive déjà (avec plus ou moins d'automatisation), et qu'on améliore constamment les outils pour le faire mieux dans le futur.
Donc il n'est pas absurde de considérer que la validation de programme relève plus de la science expérimentale que des maths. Et Rice est en partie en cause dans cet état de fait.
Considérer la validation de programme par une démarche expérimentale n'a rien d'absurde, c'est raisonnable et intéressant. Par contre tu ne peux pas invoquer le théorème de Rice pour justifier que c'est la seule approche possible.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par gasche . En réponse à la dépêche OCaml 4.03. Évalué à 3.
On arrive déjà à prouver corrects des programmes non-triviaux aujourd'hui : des compilateurs, des micro-noyaux, des machines virtuelles, des algorithmes concurrents et distribués, des noyaux de navigateur web, et j'en passe. On ne fait pas de la vérification "tout automatique" (qu'est-ce que ce ça veut dire ?), on définit des spécifications et on essaie d'automatiser au maximum la vérification que l'implémentation lui correspond. Le théorème de Rice ne dit rien sur ce qui se passe dans ce cadre, et ça ne semble pas impossible en pratique puisqu'on y arrive déjà (avec plus ou moins d'automatisation), et qu'on améliore constamment les outils pour le faire mieux dans le futur.
Considérer la validation de programme par une démarche expérimentale n'a rien d'absurde, c'est raisonnable et intéressant. Par contre tu ne peux pas invoquer le théorème de Rice pour justifier que c'est la seule approche possible.