Effectivement, la force des langages comme OCaml ou Haskell est la puissance sémantique de leur système de types. Outre la garantie qu'il n'y aura pas d'erreurs de typage à l'exécution (ce qui était ici reproché à python, mais ne les distingue pas de langage comme le C si l'on passe sous silence l'absence d'effets de bord), le système est un sous-ensemble riche du calcul propositionnel du second ordre : ce qui offre de plus un bon contrôle sémantique sur le code, mais ne dispense pas des tests unitaires.
Pour se dispenser complètement de ces derniers, il faut passer à Coq qui lui à tout le calcul des prédicats du second ordre avec logique intuitionniste (sans raisonnement par l'absurde, quoi que on peut même activer ce dernier mais là...).
Pour ceux qui ne connaissent pas ces notions, disons qu'on peut par exemple exprimer dans le système de types de Coq que l'on définit une fonction qui prend un entier et renvoie son double. Autrement dit on peut exprimer complètement la sémantique du code, et le système vérifie que le code correspond bien à sa sémantique. D'une certaine façon, un code Coq qui compile est garantie sans bugs.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le web
Posté par kantien . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 4. Dernière modification le 11 septembre 2015 à 17:54.
Effectivement, la force des langages comme OCaml ou Haskell est la puissance sémantique de leur système de types. Outre la garantie qu'il n'y aura pas d'erreurs de typage à l'exécution (ce qui était ici reproché à python, mais ne les distingue pas de langage comme le C si l'on passe sous silence l'absence d'effets de bord), le système est un sous-ensemble riche du calcul propositionnel du second ordre : ce qui offre de plus un bon contrôle sémantique sur le code, mais ne dispense pas des tests unitaires.
Pour se dispenser complètement de ces derniers, il faut passer à Coq qui lui à tout le calcul des prédicats du second ordre avec logique intuitionniste (sans raisonnement par l'absurde, quoi que on peut même activer ce dernier mais là...).
Pour ceux qui ne connaissent pas ces notions, disons qu'on peut par exemple exprimer dans le système de types de Coq que l'on définit une fonction qui prend un entier et renvoie son double. Autrement dit on peut exprimer complètement la sémantique du code, et le système vérifie que le code correspond bien à sa sémantique. D'une certaine façon, un code Coq qui compile est garantie sans bugs.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.