Je ne connais pas cette personne ni ce langage mais je ne comprends pas ce que "premier langage fonctionnel auto-prouvé (!), à la compilation" signifie.
Le terme est en effet inexact.
Quand à jeter curry-howard à la poubelle, cela provient de sa conviction que la théorie des topos est plus puissante que la théorie classiquement utilisée en Haskell, Caml, etc...
Je cite :
"prétendre qu'il y a 'isomorphisme' (c'est à dire similitude parfaite) entre preuves et programmes conduit à concevoir des systèmes formels dans lequels aucune notion correcte de sous-ensemble ne peut être définie. C'est un fait dont les logiciens et théoriciens de l'informatique commencent tout juste à prendre conscience aujourd'hui. Des langages avec preuve comme LEGO ou COQ souffrent de ce problème, qui rend quasiment impossible la manipulation de sous-ensemble ou d'ensemble quotients. Il faut donc abandonner l'isomorphisme de Curry-Howard. La théorie des topos donne une bien meilleure modélisation de ces questions."
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Ontologia (site web personnel) . En réponse à la dépêche Sortie de la version 2.5 du langage Tom. Évalué à 1.
Le terme est en effet inexact.
Je te renvoi à ce document, qui est une conférence d'Alain Prouté à l'université de Marseilles.
http://www.math.jussieu.fr/~alp/luminy_05_2007.pdf
Quand à jeter curry-howard à la poubelle, cela provient de sa conviction que la théorie des topos est plus puissante que la théorie classiquement utilisée en Haskell, Caml, etc...
Je me suis planté de lien, aussi vais-je corriger mon erreur.
Il explique ici, pourquoi il faut abandonner Curry-Howard
http://www.developpez.net/forums/showthread.php?t=46904&(...)
Je cite :
"prétendre qu'il y a 'isomorphisme' (c'est à dire similitude parfaite) entre preuves et programmes conduit à concevoir des systèmes formels dans lequels aucune notion correcte de sous-ensemble ne peut être définie. C'est un fait dont les logiciens et théoriciens de l'informatique commencent tout juste à prendre conscience aujourd'hui. Des langages avec preuve comme LEGO ou COQ souffrent de ce problème, qui rend quasiment impossible la manipulation de sous-ensemble ou d'ensemble quotients. Il faut donc abandonner l'isomorphisme de Curry-Howard. La théorie des topos donne une bien meilleure modélisation de ces questions."
Pour une comparaison avec les systèmes de type d'Haskell et d'Anubis, il explique cela ici :
http://www.developpez.net/forums/showpost.php?p=513888&p(...)
En espérant t'avoir éclairé.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker