Het artikel beschrijft de ongebruikelijke totstandkoming van een wetenschappelijke publicatie over type-systemen. De auteur was aanvankelijk de reviewer die een artikel van Leslie Lamport — waarin hij stelde dat types in specificatielangages schadelijk zijn — afwees vanwege technische onnauwkeurigheden.
Op voordracht van de redacteur besloot de auteur echter als co-auteur aan te sluiten om het stuk technisch correct te maken, terwijl de geest van Lamports stelling behouden bleef. Ondanks een moeizaam proces met verschillende redacteuren en reviewers, werd het artikel uiteindelijk gepubliceerd.
Terugblikkend concludeert de auteur dat de stelling van Lamport niet stand heeft gehouden. Moderne projecten zoals de CompCert C-compiler en seL4 tonen aan dat type-systemen juist essentieel zijn voor verificatie op industriële schaal, terwijl ongetypeerde formalismen vaak leiden tot fouten.
Hoe ik dát artikel met Leslie Lamport kwam te schrijven
Leslie Lamport heeft naam gemaakt in gedistribueerde systemen en fouttolerantie. Voor velen is hij echter bekender als de auteur van LaTeX, het beroemde macro-pakket dat het legendarische TeX-opmaaksysteem van Donald Knuth bruikbaar maakte voor de rest van ons.
Terwijl Leslie ouder werd, voelde hij zich geroepen om een reeks vrij excentrieke artikelen te schrijven met titels als "How to Write a Long Formula". Een ander van deze artikelen heette "Types Considered Harmful", een diatribe tegen types in specificatielangages. De titel was een echo van een beroemde brief van Edsger Dijkstra: "Go To Statement Considered Harmful". De titel van die brief (gekozen door de redacteur van het tijdschrift) werd vervolgens door veel auteurs overgenomen die tegen allerlei zaken waren.
Leslie was tegen types. Maar hoe ben ik hierbij betrokken geraakt?
Types als schadelijk beschouwd
Leslie's stelling was dat specificatielangages gebaseerd zouden moeten zijn op een ongetypeerd formalisme (een soort verzamelingentheorie) in plaats van een getypeerd formalisme. Hij voerde verschillende argumenten aan: ongetypeerde formalismen waren flexibeler; getypeerde formalismen zorgden voor talloze anomalieën en problemen; en wat wij zouden beschouwen als een typefout in een specificatie, zou sowieso tijdens de verificatie worden opgemerkt.
Er zat enige logica in deze stelling. Type-systemen waren in 1992, toen die notitie werd geschreven, in een staat van flux. Coq (nu Rocq) was net verschenen en er vonden grote veranderingen plaats in de type-theorie van Martin-Löf. Wat betreft eenvoudige type-theorieën: vroege implementaties van HOL bestonden pas een paar jaar. Het was niet duidelijk wat een getypeerde calculus precies kon doen. Proof assistants ondersteunden nog geen type-classes. John Harrison was nog jaren verwijderd van het introduceren van zijn truc om low-budget afhankelijke types (dependent types) te krijgen, wat goed genoeg werkt om $T^n$ uit te drukken.
Aan de andere kant was de notitie van Lamport een puinhoop. Hij leek onbekend met elk daadwerkelijk getypeerd formalisme en wijdde het grootste deel van zijn tekst aan het neerhalen van stroman-argumenten. Toen hij zijn notitie ter publicatie indiende bij TOPLAS en deze bij mij terechtkwam als reviewer, was mijn oordeel: afwijzen. De andere reviewer, David McAllester, kwam tot hetzelfde oordeel.
Dat had het einde moeten zijn, maar de redacteur, Andrew Appel, had andere ideeën.
"Er een laagje make-up over doen"
Debat is goed, zei hij. Deze ideeën verdienen het om geuit te worden, of iets in die richting. Maar we kunnen geen fouten toestaan in TOPLAS. Waarom sluit je je niet aan bij Lamport als co-auteur om het artikel om te vormen tot iets dat technisch accuraat is, maar wel in dezelfde geest is geschreven?
Ik was bereid dit te doen: ik wist veel van type-systemen en ik had ook mijn eigen ongetypeerde verzamelingentheoretische formalisme (Isabelle/ZF), dat ik graag wilde promoten. David deed een tijdje mee, maar haakte al snel af. Hij was slim.¹
Leslie en ik werkten een geruime tijd aan het artikel. Het was een vreemde vorm van onwillige co-auteurschap, maar op de een of andere manier lukte het. Het nieuwe artikel vatte de kern van Leslie's stelling samen, maar bevatte een verstandigere beschrijving van hoe types werkten. Tijdens dit proces was ik getuige van Leslie's ongeëvenaarde TeX-beheersing: low-level trucjes die ik daarna nooit meer ben tegengekomen.
Een tweede reviewronde, hemel help
Ondertussen was Andrew Appel teruggetreden als redacteur van TOPLAS. De nieuwe redacteur, Carl Gunter, was niet op de hoogte gesteld van de speciale status van dit artikel. Wanneer het artikel hem dus bereikte, stuurde hij het naar nieuwe reviewers.
Dit was niet onderdeel van het plan. En de nieuwe reviewers besloten het artikel ook af te wijzen. Een van de rapporten was incoherent; het was overduidelijk geschreven terwijl de auteur leed aan een aanval van apoplexie.
Ik nam contact op met Carl en zei: "Wacht eens even, mijn afwijzing is niets waard en de afwijzing van deze man is op somehow geldig? Bovendien is hij letterlijk krankzinnig." Uiteindelijk werd het artikel toch gepubliceerd, met een disclaimer waarin werd uitgesproken dat men hoopte op een levendig debat, enzovoort.
Ik weet niet zeker of dat debat ooit heeft plaatsgevonden.
Terugblikkend
We kunnen ons nu afvragen hoe goed Leslie's stelling 27 jaar later standhoudt. Het is eerlijk om te zeggen: niet zo goed. Type-systemen zijn aanzienlijk geëvolueerd en hebben hun waarde bewezen in talloze specificatie- en verificatietaken, sommige op industriële schaal:
- de CompCert geverifieerde C-compiler;
- seL4: "zowel de meest hoogwaardig verzekerde als de snelste operating system kernel ter wereld";
- Amazon’s Nitro Isolation Engine.
Ondertussen is er weinig vooruitgang geboekt op de problemen die verzamelingentheoretische formalismen plagen. Zonder types heb je geen overbelasting (overloading) van notaties, wat in principe triviaal is (je kunt gewoon veel verschillende symbolen gebruiken), maar in de praktijk een groot probleem is.
En erger nog: de mogelijkheid om absoluut alles op te schrijven is vooral een uitnodiging om fouten te maken. Verificatie is een extreem dure manier om dergelijke fouten te vinden, en de fouten die je niet vindt, kunnen je bewijzen waardeloos maken.
Voor zover ik weet, is zelfs de eigen specificatielangage van Lamport (TLA+) uiteindelijk geïmplementeerd met enkele type-beperkingen. Dus, in feite zou je specificatielangage waarschijnlijk getypeerd moeten zijn. Maar het is nog steeds de moeite waard om te zoeken naar manieren om verzamelingentheoretische notaties beter te laten werken.
***
¹ Hoewel er geen noodzaak voor hem was om de Hitler-kaart te trekken.
Hoe ik dát artikel met Leslie Lamport kwam te schrijven
Leslie Lamport heeft naam gemaakt in gedistribueerde systemen en fouttolerantie. Voor velen is hij echter bekender als de auteur van LaTeX, het beroemde macro-pakket dat het legendarische TeX-opmaaksysteem van Donald Knuth bruikbaar maakte voor de rest van ons.
Terwijl Leslie ouder werd, voelde hij zich geroepen om een reeks vrij excentrieke artikelen te schrijven met titels als "How to Write a Long Formula". Een ander van deze artikelen heette "Types Considered Harmful", een diatribe tegen types in specificatielangages. De titel was een echo van een beroemde brief van Edsger Dijkstra: "Go To Statement Considered Harmful". De titel van die brief (gekozen door de redacteur van het tijdschrift) werd vervolgens door veel auteurs overgenomen die tegen allerlei zaken waren.
Leslie was tegen types. Maar hoe ben ik hierbij betrokken geraakt?
Types als schadelijk beschouwd
Leslie's stelling was dat specificatielangages gebaseerd zouden moeten zijn op een ongetypeerd formalisme (een soort verzamelingentheorie) in plaats van een getypeerd formalisme. Hij voerde verschillende argumenten aan: ongetypeerde formalismen waren flexibeler; getypeerde formalismen zorgden voor talloze anomalieën en problemen; en wat wij zouden beschouwen als een typefout in een specificatie, zou sowieso tijdens de verificatie worden opgemerkt.
Er zat enige logica in deze stelling. Type-systemen waren in 1992, toen die notitie werd geschreven, in een staat van flux. Coq (nu Rocq) was net verschenen en er vonden grote veranderingen plaats in de type-theorie van Martin-Löf. Wat betreft eenvoudige type-theorieën: vroege implementaties van HOL bestonden pas een paar jaar. Het was niet duidelijk wat een getypeerde calculus precies kon doen. Proof assistants ondersteunden nog geen type-classes. John Harrison was nog jaren verwijderd van het introduceren van zijn truc om low-budget afhankelijke types (dependent types) te krijgen, wat goed genoeg werkt om $T^n$ uit te drukken.
Aan de andere kant was de notitie van Lamport een puinhoop. Hij leek onbekend met elk daadwerkelijk getypeerd formalisme en wijdde het grootste deel van zijn tekst aan het neerhalen van stroman-argumenten. Toen hij zijn notitie ter publicatie indiende bij TOPLAS en deze bij mij terechtkwam als reviewer, was mijn oordeel: afwijzen. De andere reviewer, David McAllester, kwam tot hetzelfde oordeel.
Dat had het einde moeten zijn, maar de redacteur, Andrew Appel, had andere ideeën.
"Er een laagje make-up over doen"
Debat is goed, zei hij. Deze ideeën verdienen het om geuit te worden, of iets in die richting. Maar we kunnen geen fouten toestaan in TOPLAS. Waarom sluit je je niet aan bij Lamport als co-auteur om het artikel om te vormen tot iets dat technisch accuraat is, maar wel in dezelfde geest is geschreven?
Ik was bereid dit te doen: ik wist veel van type-systemen en ik had ook mijn eigen ongetypeerde verzamelingentheoretische formalisme (Isabelle/ZF), dat ik graag wilde promoten. David deed een tijdje mee, maar haakte al snel af. Hij was slim.¹
Leslie en ik werkten een geruime tijd aan het artikel. Het was een vreemde vorm van onwillige co-auteurschap, maar op de een of andere manier lukte het. Het nieuwe artikel vatte de kern van Leslie's stelling samen, maar bevatte een verstandigere beschrijving van hoe types werkten. Tijdens dit proces was ik getuige van Leslie's ongeëvenaarde TeX-beheersing: low-level trucjes die ik daarna nooit meer ben tegengekomen.
Een tweede reviewronde, hemel help
Ondertussen was Andrew Appel teruggetreden als redacteur van TOPLAS. De nieuwe redacteur, Carl Gunter, was niet op de hoogte gesteld van de speciale status van dit artikel. Wanneer het artikel hem dus bereikte, stuurde hij het naar nieuwe reviewers.
Dit was niet onderdeel van het plan. En de nieuwe reviewers besloten het artikel ook af te wijzen. Een van de rapporten was incoherent; het was overduidelijk geschreven terwijl de auteur leed aan een aanval van apoplexie.
Ik nam contact op met Carl en zei: "Wacht eens even, mijn afwijzing is niets waard en de afwijzing van deze man is op somehow geldig? Bovendien is hij letterlijk krankzinnig." Uiteindelijk werd het artikel toch gepubliceerd, met een disclaimer waarin werd uitgesproken dat men hoopte op een levendig debat, enzovoort.
Ik weet niet zeker of dat debat ooit heeft plaatsgevonden.
Terugblikkend
We kunnen ons nu afvragen hoe goed Leslie's stelling 27 jaar later standhoudt. Het is eerlijk om te zeggen: niet zo goed. Type-systemen zijn aanzienlijk geëvolueerd en hebben hun waarde bewezen in talloze specificatie- en verificatietaken, sommige op industriële schaal:
- de CompCert geverifieerde C-compiler;
- seL4: "zowel de meest hoogwaardig verzekerde als de snelste operating system kernel ter wereld";
- Amazon’s Nitro Isolation Engine.
Ondertussen is er weinig vooruitgang geboekt op de problemen die verzamelingentheoretische formalismen plagen. Zonder types heb je geen overbelasting (overloading) van notaties, wat in principe triviaal is (je kunt gewoon veel verschillende symbolen gebruiken), maar in de praktijk een groot probleem is.
En erger nog: de mogelijkheid om absoluut alles op te schrijven is vooral een uitnodiging om fouten te maken. Verificatie is een extreem dure manier om dergelijke fouten te vinden, en de fouten die je niet vindt, kunnen je bewijzen waardeloos maken.
Voor zover ik weet, is zelfs de eigen specificatielangage van Lamport (TLA+) uiteindelijk geïmplementeerd met enkele type-beperkingen. Dus, in feite zou je specificatielangage waarschijnlijk getypeerd moeten zijn. Maar het is nog steeds de moeite waard om te zoeken naar manieren om verzamelingentheoretische notaties beter te laten werken.
***
¹ Hoewel er geen noodzaak voor hem was om de Hitler-kaart te trekken.
Groetjes,