Le problème que nous sommes en train de discuter est de savoir si un programme correspond à sa spécification, elle-même décrite dans un langage fixé. En particulier, on ne regarde pas une propriété fixée sur tous les programmes, mais une propriété différente pour chaque programme.
Oui, enfin il existe un sous-ensemble de propriétés désirés qui sont les mêmes pour tout les programmes. "Mon programme risque-t-il de planter à l'exécution ?" en est une belle. Et cette propriété peut s'exprimer dans le cadre du théorème de Rice. Soit M une machine de Turing. Le langage reconnu par M est l'ensemble des entrées w pour lesquels m termine sans planter1. Savoir si ce langage est l'ensemble des entrées est indécidable. Dit autrement, conséquence de Rice : un compilateur ne peut pas garantir que ton programme ne plantera pas à l'exécution ni qu'il termine. Donc cela n'a pas "rien à voir". Et c'est ce que je dis depuis le début, on ne peut pas laisser la preuve à un compilateur, on est obligé de se la farcir soi-même.
Alors certes, tu va me dire que OCaml (si on ne fait que du fonctionnel) permet d'éviter cela. Mais peut-on éviter les débordements de pile avec du typage ? Peut-il empêcher les récurrences infinis ? Peut-il garantir qu'aucune branche ne contenant une exception ne sera jamais atteinte ?
Je n'ai jamais dis que les preuves de programme était impossible, ni qu’elles étaient inutiles. Ce serait stupide. Mais qu'à priori, elle ne seront jamais suffisante pour garantir l’absence de bug (même si elle permettent d'en limiter un grand nombre). Je serais fort étonné que l'on arrive un jour à passer outre tous les problèmes d'impossibilité avec du typage (puisqu’en fait, tu propose de cacher la démonstration dans le typage). Et quand bien même ce serait possible, alors cela voudrait dire que le système de typage serait devenue bien trop affreux et contraignant pour la majorité des usages.
Si tu prends ma phrase du début :
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
Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique) . Et enfin je n'ai jamais dit que les systèmes de preuves était inutile mais insuffisant. J'ai un peu l'impression que tu me reproche une posture extrême "les preuves en info sont impossibles" alors que depuis le début je parle simplement de la nécessité d'avoir à utiliser des outils complémentaires.
[1] je sais que le concept de plantage n'existe pas en machine de Turing mais il pourrait se définir sans difficulté aucune.
[^] # 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é à 3.
Oui, enfin il existe un sous-ensemble de propriétés désirés qui sont les mêmes pour tout les programmes. "Mon programme risque-t-il de planter à l'exécution ?" en est une belle. Et cette propriété peut s'exprimer dans le cadre du théorème de Rice. Soit M une machine de Turing. Le langage reconnu par M est l'ensemble des entrées w pour lesquels m termine sans planter1. Savoir si ce langage est l'ensemble des entrées est indécidable. Dit autrement, conséquence de Rice : un compilateur ne peut pas garantir que ton programme ne plantera pas à l'exécution ni qu'il termine. Donc cela n'a pas "rien à voir". Et c'est ce que je dis depuis le début, on ne peut pas laisser la preuve à un compilateur, on est obligé de se la farcir soi-même.
Alors certes, tu va me dire que OCaml (si on ne fait que du fonctionnel) permet d'éviter cela. Mais peut-on éviter les débordements de pile avec du typage ? Peut-il empêcher les récurrences infinis ? Peut-il garantir qu'aucune branche ne contenant une exception ne sera jamais atteinte ?
Je n'ai jamais dis que les preuves de programme était impossible, ni qu’elles étaient inutiles. Ce serait stupide. Mais qu'à priori, elle ne seront jamais suffisante pour garantir l’absence de bug (même si elle permettent d'en limiter un grand nombre). Je serais fort étonné que l'on arrive un jour à passer outre tous les problèmes d'impossibilité avec du typage (puisqu’en fait, tu propose de cacher la démonstration dans le typage). Et quand bien même ce serait possible, alors cela voudrait dire que le système de typage serait devenue bien trop affreux et contraignant pour la majorité des usages.
Si tu prends ma phrase du début :
Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique) . Et enfin je n'ai jamais dit que les systèmes de preuves était inutile mais insuffisant. J'ai un peu l'impression que tu me reproche une posture extrême "les preuves en info sont impossibles" alors que depuis le début je parle simplement de la nécessité d'avoir à utiliser des outils complémentaires.
[1] je sais que le concept de plantage n'existe pas en machine de Turing mais il pourrait se définir sans difficulté aucune.