Was ist die „Frage“, die die Programmiersprachentheorie zu beantworten versucht?

Ich habe mich eine Weile für verschiedene Themen wie kombinatorische Logik, Lambda-Kalkül und funktionale Programmierung interessiert und sie studiert. Im Gegensatz zur "Theorie der Berechnung", die versucht, die Frage der "Berechenbarkeit" zu beantworten, dh Dinge, die mit verschiedenen Einschränkungen berechnet werden können / nicht, habe ich Schwierigkeiten, das Analogon für "Theorie der Programmierung" zu finden.

Wikipedia beschreibt es als:

Die Programmiersprachentheorie (PLT) ist ein Zweig der Informatik, der sich mit dem Entwurf, der Implementierung, Analyse, Charakterisierung und Klassifizierung von Programmiersprachen und ihren individuellen Merkmalen befasst.

Dies ist wie "alles" zu sagen, was nicht wirklich spezifisch ist.

Der gemeinsame Verlauf der Themen ist normalerweise wie folgt:

Kombinatorische Logik> Lambda-Rechnung> Martin-Lof-Typentheorie> Typisierte Lambda-Rechnung> (hier passiert etwas)> Entwickelte Programmiersprachen - die nur sehr wenig mit CL / λ zu tun haben$\lambda$

$\lambda$

$\lambda$

Der allgemeine Zweck von PLT besteht darin, das industrielle Software-Engineering (im Allgemeinen) (auch im Allgemeinen) billiger zu machen , indem das wichtigste Werkzeug (Programmiersprachen) und das damit verbundene Werkzeug-Ökosystem optimiert werden.

Einige Gründe, warum Mathematik eine Rolle spielt:

• PLs sind höchst nicht trivial, und es ist nicht klar, dass sie ohne Beweise das Richtige tun. Die Mathematik liefert ein vereinfachtes Modell realer Programmiersprachen. Mit diesem Modell können wir echte Programmiersprachen in einer stark vereinfachten Umgebung lernen und (hoffentlich) die meisten Probleme bereits auf Modellebene beseitigen. Echte Programmiersprachen sind derzeit mathematisch nicht umsetzbar. Mit anderen Worten: Lambda-Kalkül ist die Fruchtfliege, die E.Coli, die kugelförmige Kuh von PLT.

• PLT fehlen geeignete empirische Methoden, die schön / besser wären, daher wird Mathematik als Ersatz verwendet.

• Die Mathematik ist schön und tief.

• Die Mathematik bietet eine einfache, erprobte und erprobte Forschungsmethode, die wichtig ist, um den Doktoranden beim Abschluss zu helfen. Typischerweise eine Variante von z. B.: Untersuchen Sie das PL-Merkmal XYZ, indem Sie es dem Lambda-Kalkül hinzufügen. Fügen Sie einfache Typen für XYZ hinzu und beweisen Sie die Typ-Solidität. Fügen Sie Generika für XYZ hinzu und beweisen Sie die Typ-Solidität. Beweisen Sie einen Parametrizitätssatz für XYZ-Generika. Fügen Sie abhängige Typen für XYZ hinzu und beweisen Sie die Typensicherheit. Entwickeln Sie eine partielle Typinferenz für XYZ-abhängige Typen. Fügen Sie schrittweise Typen für XYZ hinzu und beweisen Sie die Typ-Solidität. Fügen Sie Verträge für XYZ hinzu. Jedes davon ist ein Papier. Sie können aufhören, wenn Ihr Doktorand oder Postdoc keine Zeit mehr hat. Jedes der oben genannten Punkte ist interessant und liefert Einblicke in Generika, Parametrizität, Typinferenz usw. Diese Pipeline ist großartigArt und Weise, durch die schwierigen Gewässer aller möglichen Programmiersprachen zu navigieren. Eine zweite Art des Lernens besteht darin, Sprachen in einem Compiler zu implementieren, was für eine Person jedoch weniger praktikabel ist.

Ob PLT benötigt wird, ist eine interessante Frage. Die meisten arbeitenden Programmierer scheinen zu glauben, dass dies nicht der Fall ist. Sie sind falsch: Die meisten Sprachen, die von arbeitenden Programmierern ohne PLT-Hintergrund entwickelt wurden (z. B. Javascript, PHP), fangen schrecklich an und machen alle Fehler, die PL-Theoretiker seit langem zu vermeiden gelernt haben. Wenn ein von einem Amateur entwickelter PL den Mainstream erreicht, müssen PL-Theoretiker etwa ein Jahrzehnt lang die offensichtlichen Mängel beheben (z. B. Nachrüstung eines statischen Typisierungssystems, siehe Typoskript). Lassen Sie mich diese Situation zusammenfassen:

 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. ;-)

^{Nebenbei: Dieser Sachverhalt ist ausschließlich die Schuld von PLT, da die meisten von ihnen keine Erfahrung in der industriellen Programmierung haben und daher nicht wirklich wissen, wo die Probleme der arbeitenden Softwareentwickler liegen. Insbesondere aus soziologischen Gründen denken die meisten PL-Theoretiker, dass reine funktionale Programmierung in Sprachen wie Agda die Lösung für alle Probleme ist, die einer Prüfung nicht standhalten.}