C'est assez typique de moi : je suis parti ce matin avec l'intention de m'acheter une bible en slavon, et finalement (après avoir fait chou blanc à la librairie du Globe et être passé chez Eyrolles sur le chemin du retour) j'ai fait l'acquisition d'un livre sur la théorie du typage (le genre de choses qui provoque chez moi des cauchemars) : Types and Programming Languages de Benjamin Pierce. J'ai passé une bonne partie de l'après-midi à le lire (pas dans les moindres détails, évidemment, car il est assez épais, mais suffisamment pour m'en faire une bonne idée et pour apprendre des choses), et je le recommande : il est tout à fait intelligemment structuré et très clair, présentant successivement tout un tas d'enrichissement du système de types d'un langage et expliquant les répercussions que cela a.
C'est quelque chose qui me perturbe dans mon idéalisme, d'ailleurs, le système de type : j'essaie de concevoir un langage de programmation idéal à mon goût (pas de l'implémenter, certainement, mais au moins de me le représenter mentalement de façon précise) et, si j'ai une idée assez nette des autres aspects du langage (en gros, ce serait un langage fonctionnel, hâtif par défaut mais optionnellement localement paresseux, avec séquencement explicite des effets de bord, possibilité de contrôler finement l'allocation de mémoire et de placer des limites sur les ressources à l'exécution, et virtualisation et réflexivité aisées, et utilisant une syntaxe à la Lisp), le typage me pose problème. Évidemment, les types doivent avoir citoyenneté de première classe (globalement, tout ce qui concerne le langage de près ou de loin doit avoir citoyenneté de première classe, sinon on perd de l'expressivité et de la réflexivité), donc le truc ressemblerait à quelque chose comme le calcul des constructions inductives avec sous-typage, en encore plus général, et sur de la logique linéaire (pour pouvoir contrôler la duplication des données, et donc l'allocation mémoire, si besoin est) ; tout ce qui ne peut pas facilement se vérifier statiquement se vérifie dynamiquement (pour moi, le typage statique ne doit être qu'une optimisation sur le typage dynamique, un peu comme le fait de remplacer 2+2 par sa valeur dans le source) et tout ce que le typeur ne peut pas inférer peut être explicitement donné par des annotations : mais les détails sont encore très flous. En fait, le typage n'est qu'un cas particulier des preuves qui peuvent être faites sur un programme, et on voudrait que le langage permette de poser et de faire vérifier (soit statiquement si c'est possible, soit dynamiquement) absolument n'importe quelle preuve de propriété que le programmeur voudra bien apporter : il faudrait que cela s'insère de façon élégante comme un mécanisme de typage, mais je ne vois pas bien comment faire.
Je ferais mieux de faire des maths, moi, c'est plus facile que l'info.