• [^] # Re: Encore le type Null...

    Posté par . En réponse à la dépêche Dart va‐t‐il remplacer JavaScript comme langage dans les navigateurs ?. Évalué à 4.

    Non, je ne pense pas que Java ait été conçu avec un modèle théorique en tête. Je ne sais pas à quoi tu fais référence en disant qu'il est "rempli de lambda-calcul".

    Ben Java est type-safe, et ça passe par du lambda calcul si tu veux le faire correctement. Tu peux avoir toutes les impressions que tu veux, ça reste vrai. Dire que Java n'a pas de modèle théorique en tête, c'est tout simplement ne pas être au courant de comment Java a été conçu. Java est un des premiers langages « grand public » qui a tenté d'intégrer le parallélisme et la concurrence dès le départ. Du point de vue théorique, ça passe par un modèle de concurrence ainsi qu'un modèle mémoire (il est démontrable que le premier modèle mémoire est cassé, et le deuxième modèle, introduit en 2005-2006, bien que bien meilleur, reste contesté, avec des papiers qui démontrent que certaines propriétés demandées par le modèles sont invérifiables).

    L'impression que j'ai est plutôt que les ingénieurs qui ont conçu Java n'étaient pas forcément très au courant de la recherche dans le domaine, mais ont surtout retiré les fonctionnalités les plus complexes de C++ pour faire un langage simplifié.

    L'un n'empêche pas l'autre. Cependant la JVM est parfaitement spécifiée, et la traduction de code Java vers le bytecode itou.

    Ensuite, dans les versions récentes de Java, l'importance pratique du langage a motivé des spécialistes de la théorie des types à se pencher sur la question des génériques notamment.

    Définis « récentes ». La théorie des types, etc., appliquée aux types / classes de Java ça fait un moment (je dirais au moins 10 ans) que c'est intégré à l'implémentation de référence. Exemple, le bouquin de B. Pierce, Types and Programming Languages, est sorti en 2002, et propose déjà un « mini-java » typesafe en guise d'exercice...

    Une simple recherche google avec les mots-clef « lambda calculus type safety java » renvoient vers le bouquin de Pierce, puis vers des rapports techniques sur la possibilité de compiler Java vers du lambda calcul typé (rapport datant de 1998).

    C'est là que sont apparus des modèles formels de sous-ensembles de Java, basés sur la recherche faite indépendamment sur la théorie des langages objets. Mais ça ne veut pas dire que Java dans son ensemble ait été conçu par des gens connaissant la théorie.

    Les mecs qui ont conçu Java n'étaient certes pas des dieux de la compilation et de la théorie des langages, mais une rapide recherche sur J.Gosling (l'un des papas de Java avec Bill Joy) montre que sa thèse de 1983 s'intitule The Algebraic Manipulation of Constraints. Bref, pas un p'tit joueur non plus.