Désolé si mon message paraissait agressif, c'était pas volontaire :) Je suis quelqu'un de gentil en fait ! Mais je ne voyais pas en quoi l'irrationalité de racine de 2 pouvait poser problème à Popper, au test unitaire ou au système de typage.
et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Là c'est un point que je maîtrise moins bien (pas au programme de l'agreg :) ) Peut on prouver faux dans un système de typage ? Il me semblait que le "faux" se traduisait par une exception à l'exécution, ou un programme que ne termine pas. Dans le cas de racine de deux, c'est une fraction qu'on simplifie infiniment par exemple. Mais peut on créer un fonction de type dont le type de retour est "faux" ?
[^] # 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.
Désolé si mon message paraissait agressif, c'était pas volontaire :) Je suis quelqu'un de gentil en fait ! Mais je ne voyais pas en quoi l'irrationalité de racine de 2 pouvait poser problème à Popper, au test unitaire ou au système de typage.
Là c'est un point que je maîtrise moins bien (pas au programme de l'agreg :) ) Peut on prouver faux dans un système de typage ? Il me semblait que le "faux" se traduisait par une exception à l'exécution, ou un programme que ne termine pas. Dans le cas de racine de deux, c'est une fraction qu'on simplifie infiniment par exemple. Mais peut on créer un fonction de type dont le type de retour est "faux" ?