Sur Popper et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens... :-)
D'un côté reprocher à Popper qui travaille sur l'épistémologiste des sciences expérimentales que son approche n'est pas adapté au math...
L'irrationalité de racine de 2 est montrable en logique intuitionniste (mathématique constructiviste qui refuse les démonstrations par l'absurde de type « si (non P => Faux) alors P » mais par contre on autorise « (P => faux) => (non P) » car en fait c'est même la définition de non P). Donc le preuve doit être transposable dans un système de typage (mais ça je ne suis pas certain). En tous cas, je ne suis pas sur que cet exemple soit le meilleur :)
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.
[^] # 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é à 5.
D'un côté reprocher à Popper qui travaille sur l'épistémologiste des sciences expérimentales que son approche n'est pas adapté au math...
L'irrationalité de racine de 2 est montrable en logique intuitionniste (mathématique constructiviste qui refuse les démonstrations par l'absurde de type « si (non P => Faux) alors P » mais par contre on autorise « (P => faux) => (non P) » car en fait c'est même la définition de non P). Donc le preuve doit être transposable dans un système de typage (mais ça je ne suis pas certain). En tous cas, je ne suis pas sur que cet exemple soit le meilleur :)
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.