Quelle est la «question» à laquelle la théorie du langage de programmation essaie de répondre?

Je m'intéresse à divers sujets comme la logique combinatoire, le calcul lambda, la programmation fonctionnelle depuis un certain temps et je les étudie. Cependant, contrairement à la «Théorie du calcul» qui s'efforce de répondre à la question de la «calculabilité», c'est-à-dire des choses qui peuvent / ne peuvent pas être calculées avec diverses contraintes, j'ai du mal à trouver l'analogue de la «Théorie de la programmation».

Wikipedia le décrit comme:

La théorie des langages de programmation (PLT) est une branche de l'informatique qui traite de la conception, de la mise en œuvre, de l'analyse, de la caractérisation et de la classification des langages de programmation et de leurs caractéristiques individuelles.

C'est comme dire "tout" qui n'est pas vraiment spécifique.

La progression commune des sujets est généralement la suivante:

Logique combinatoire> Calcul lambda> Théorie des types de Martin Lof> Calcul lambda typé> (Quelque chose se passe ici)> Langages de programmation développés - qui ont très peu de connexion avec CL / $\lambda$

$\lambda$

$\lambda$

L'objectif général du PLT est de rendre le génie logiciel industriel (au sens général) moins cher (également au sens général), en optimisant l'outil le plus important (langages de programmation) et l'écosystème d'outillage associé.

Quelques raisons pour lesquelles les mathématiques sont impliquées:

• Les PL sont très non triviaux, et il n'est pas clair qu'ils fassent la bonne chose sans preuve. Les mathématiques donnent un modèle simplifié de vrais langages de programmation. Ce modèle nous permet d'étudier de vrais langages de programmation dans un cadre beaucoup plus simplifié, supprimant (espérons-le) la plupart des problèmes déjà au niveau du modèle. Les vrais langages de programmation sont actuellement mathématiquement insolubles. En d'autres termes: le lambda-calcul est la mouche des fruits, l'E. Coli, la vache sphérique du PLT.

• Le PLT manque de méthodes empiriques appropriées, ce qui serait bien / mieux d'avoir, donc les mathématiques sont faites comme substitut.

• Les mathématiques sont belles et profondes.

• Les mathématiques donnent une méthodologie de recherche simple, éprouvée et testée, qui est importante pour aider ses étudiants au doctorat à obtenir leur diplôme. Typiquement, une variante de par exemple: Investigate PL feature XYZ en l'ajoutant au lambda-calcul. Ajoutez des types simples pour XYZ et prouvez la validité des caractères. Ajoutez des génériques pour XYZ et prouvez la validité des caractères. Démontrer un théorème de paramétrie pour les génériques XYZ. Ajoutez des types dépendants pour XYZ et prouvez la validité des caractères. Développer une inférence de type partielle pour les types dépendants de XYZ. Ajoutez des types progressifs pour XYZ et prouvez la validité des caractères. Ajoutez des contrats pour XYZ. Chacun d'eux est un document. Vous pouvez vous arrêter si votre doctorant ou post-doctorant manque de temps. Chacun des éléments ci-dessus est intéressant et donnera des informations sur les génériques, la paramétricité, l'inférence de type, etc. Ce pipeline est un excellentfaçon de naviguer dans les eaux difficiles de tous les langages de programmation possibles. Une deuxième façon d'apprendre consiste à implémenter des langages dans un compilateur, mais c'est moins maniable pour un individu.

La nécessité du PLT est une question intéressante. La plupart des programmeurs qui travaillent semblent penser que non. Ils ont tort: ​​la plupart des langages développés par des programmeurs actifs sans expérience PLT (par exemple Javascript, PHP) commencent terriblement et font toutes les erreurs que les théoriciens du PL ont longtemps appris à éviter. Si un PL développé par un amateur atteint le courant dominant, les théoriciens du PL ont besoin d'une dizaine d'années pour corriger les défauts évidents (par exemple, moderniser un système de typage statique, voir Typescript). Permettez-moi de résumer cette situation:

 Every successful programming language ends up being ML! Either because 
 it was designed by a PL theorist as ML from the start, or because a 
 decade of painful evolution removes all the obvious flaws, leaving ML. ;-)

^{À part: Cet état de fait est entièrement la faute du PLT car parce que la plupart d'entre eux n'ont aucune expérience en programmation industrielle, alors je ne sais pas vraiment quels sont les points faibles des ingénieurs logiciels qui travaillent. En particulier, pour des raisons sociologiques, la plupart des théoriciens du PL pensent que la programmation fonctionnelle pure dans des langages comme Agda est la solution à tous les problèmes, ce qui ne résiste pas à l'examen.}