Wie ich mit Leslie Lamport genau jenes Paper schrieb
I came to write THAT paper with Leslie Lamport
Lawrence C. Paulson erzählt, wie er unfreiwillig Mitautor von Leslie Lamports umstrittenem Paper „Types Considered Harmful“ wurde. Ursprünglich als Gutachter abgelehnt, wurde er vom Herausgeber Andrew Appel gedrängt, das Paper mit Lamport zu überarbeiten. Nach einer zweiten Ablehnungsrunde erschien es schließlich doch. Paulson zieht Bilanz: Typisierte Formalismen haben sich bewährt, während die Probleme untypisierter Systeme bestehen bleiben.
Ohne Typen hat man keine Überladung von Notation, was prinzipiell trivial ist (man kann einfach viele verschiedene Symbole verwenden), aber in der Praxis eine große Sache ist.
- joomy
Irgendwie ist die finale Version des Papers nicht im Blogbeitrag verlinkt: https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> Der andere Gutachter, David McAllester, kam zum selben Urteil.
Derselbe David McAllester, der die PAC-Bayes'schen Schranken eingeführt hat?
Antwort: Ja.
- mrkeen
> In dieser These steckte etwas Sinn. Typsysteme waren 1992, als diese Notiz geschrieben wurde, im Fluss. Coq (jetzt Rocq) war gerade erst erschienen, und es gab große Veränderungen in der Martin-Löf-Typentheorie. Was einfache Typentheorien betrifft, so gab es frühe Implementierungen von HOL erst seit ein paar Jahren. Es war nicht klar, was irgendein typisierter Kalkül leisten konnte. Beweisassistenten unterstützten noch keine Typklassen. John Harrison war noch Jahre davon entfernt, seinen Trick für Low-Budget-abhängige Typen einzuführen, der gut genug funktioniert, um Tn auszudrücken.
Ich möchte weder lineare noch abhängige Typen in TLA+ einbauen. Das Beweisen dynamischer Eigenschaften mit einer erschöpfenden Laufzeit ist ein völlig anderes Spiel als das, was man statisch machen könnte.
Aber ich möchte sehr wohl Unsinn ausschließen. Klar, ich kann beweisen, dass eine Ampel nie ROT_LICHT ist. Schade, wenn sie ROT ist.