welle::erd.ferkel

Leslie Lamport, bei uns hier vor allem bekannt für L^AT_EX, hielt gestern bei uns einen Vortrag mit dem schönen Titel “Thinking for Programmers”. Der angenehm reißerische Text der Einladung

There is a very effective software development tool that is not used nearly enough—the brain. The many impediments to its proper use devised by computer scientists can be overcome.

Wahrscheinlich gibt es irgendwo eine Vorschrift, die genau regelt, wie Vorträge über Softwareentwicklung abzulaufen haben, jedenfalls habe ich in den letzten Jahren ein gewisses Grundprinzip entdeckt. Zuerst stellt man fest, dass Softwareentwicklung im Allgemeinen viel zu unstrukturiert und unzuverlässig abläuft, dann kommen ein paar Fallbeispiele (z.B. die Ariane 5) oder, was gestern der Fall war, einfach nur allgemeine Vergleiche zu den richtigen Ingenieuren (“Wenn die so Brücken bauen würden, wie programmiert wird”), um dann schließlich eine Lösung vorzuschlagen, die meistens irgendwo zwischen den zwei bekannten Extremen “Korrektheit vom Anfang bis zum Ende beweisen” (dem Theoretiker-Ansatz) bzw. “Entwicklungsprozess beschreiben und Bilder malen” (dem Software-Engineering-Ansatz) liegen.

Lamport folgte auch diesem Schema, sein Lösungsrezept ist nun aber eher so etwas wie “Man sollte formal genau aufschreiben, was die Programme tun sollen, das langt dann schon. Alle Anforderungen komplett zu beschreiben ist Arbeit. Von uns hier macht das doch keiner täglich.”. Darauf folgte dann ziemliches Gelächter, denn immerhin waren im Publikum mindestens 5 Professoren (samt Anhang), die eben genau das täglich machen (lassen). Sein Pech, dass das ein gemeinsames Kolloquium mit Saarbrücken war, denn da wird der Hardcore-Ansatz besonders überzeugt vertreten.

Ziemlich schnell bekam ich dann den Eindruck, dass Lamport für eine andere Zielgruppe als die Anwesenden vortrug. Was er uns erzählte war, warum Programmierer seiner Meinung nach formaler Denken sollten, aber abgesehen von dem einen oder anderen überforderten Softwareingenieur ist da schon im Voraus jeder seiner Meinung. Stattdessen hätte ich gerne gehört, warum er die Formalisierung klein halten will und warum die Mathematik, die er in der Schule gelernt hat, vollkommen ausreichend sein soll; das alles ging in dem “Leute, drückt euch formaler aus, das ist wichtig” aber vollkommen unter.

Insgesamt war das ganze zwar nicht wirklich bildend, aber doch ganz lustig, und immerhin hat er zugegeben, dass es noch einige Zeit dauern dürfte, bis Microsoft (sein Arbeitgeber) auch nur ansatzweise formaler arbeiten wird. Aber wenn Bill Gates selbst schon großes Interesse angemeldet hat kann das ja nicht mehr soo lange dauern, nicht wahr? Abgesehen davon war es ganz nett, mal keinen Stuhlplatz mehr zu kriegen und deswegen auf einem Tisch zu sitzen, das kommt bei Vorträgen eher selten vor.

Um in diese ganze “Bloggerei” mal wieder reinzukommen, und als Einstimmung für nächste Woche:

That’s no moon. That’s a melon. The Death Melon!

¹ Was nicht geringschätzig gemeint ist, wohl aber so klingt.