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

10

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λ

λ

λ

PhD
quelle
1
λ
λ
2
π

Antworten:

13

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.

Martin Berger
quelle
1
@MartinBerger: Zählt CompCert als Beispiel dafür, wie man "theoretisch" mit einer realen Programmiersprache umgehen kann? Wenn nicht, wie hoch setzen Sie die Messlatte, denn CompCert ist ziemlich beeindruckend.
Andrej Bauer
2
@MartinBerger: Bitte denken Sie daran, "die meisten PL-Theoretiker glauben, dass reine funktionale Programmierung in Sprachen wie Agda die Lösung für alle Probleme ist", denn das ist nur Ihr Schimpfen und Entlüften. Selbst wenn Sie sich die Themen ansehen, die derzeit bei ICFP und POPL aktuell sind, geht es bei der Mehrheit zunächst um unreine Programmiersprachen.
Andrej Bauer
5
@PhD: PLT bietet viel mehr als nur Typentheorie. Es ist nur so, dass die Typentheorie das erste ist, was Sie bemerken, weil sie eines der Hauptwerkzeuge von PLT ist.
Andrej Bauer
1
@AndrejBauer CompCert, CakeML usw. sind beeindruckend, aber sie sind weit entfernt von weit verbreiteten Compilern wie LLVM, GCC usw. Darüber hinaus haben Compiler im Gegensatz zu fast jeder realen Software eine (Art / Art) Spezifikation. was man in der normalen industriellen Softwareentwicklung einfach nicht bekommt. Ganz zu schweigen davon, dass ein großer Teil von Xaviers frühen Arbeiten zu CompCert darin bestand, die Spezifikation genau zu präzisieren.
Martin Berger
2
@PhD In Bezug auf "" radikal produktiver "als> Nicht-PLT C / C ++, Java, C #" denken Sie bitte daran, dass, wenn Sie sich diese Sprachen genauer ansehen, ihre Entwicklung im Laufe der Zeit, fast alles, was sie erworben haben Zeit, zB Lambdas, Monaden (LINQ), Mustervergleich, partielle Typinferenz, kommt von PLT. Das C # -Team hat PLT-Doktortitel. Tatsächlich haben sie versucht, mich irgendwann einzustellen. Das Vorstellungsgespräch war mein Versuch, Anders Heijlsberg davon zu überzeugen, dass C # Generika braucht, die er damals nicht mochte ...
Martin Berger