Moderne Betriebssysteme zeichnen sich dadurch aus, dass sie automatische Update-Funktionen besitzen. Ohne Zutun des Benutzers werden aktualisierte Versionen auf geradezu gespenstische Weise im Hintergrund geladen und installiert. »Aktualisierte Versionen« ist dabei die höfliche Formulierung von »Fehlerbehebungen«. Vor Kurzem teilte mir nun mein Rechner mit, er könne das Betriebssystem Update leider nicht einspielen, da dieses mindestens 4,6 GB freien Speicher benötige. Etwas überspitzt formuliert, aber mit einem Körnchen Wahrheit: Die Firma Apple hielt es für nötig, über vier Milliarden Byte an Fehlern zu korrigieren. Da wundert es wahrlich, dass Computer überhaupt irgendetwas richtig machen.
Was die Menschheit an fehlerhafter Software ertragen muss, ist eigentlich unfassbar. Würde sich die Architektur eine solche Fehlerfülle erlauben, so würden in Großstädten wöchentlich ganze Stadtteile aufgrund von Statikfehlern in sich zusammenbrechen. Würde sich die Automobilindustrie solche Schnitzer erlauben, müsste die Höchstgeschwindigkeit auf Autobahnen aus Sicherheitsgründen auf 5 km/h beschränkt sein. Würde die Luftfahrtindustrie Flugzeuge genauso wie Software bauen, würden Sie am Eingang eines Fliegers vorsichtshalber zwei Fallschirme ausgehändigt bekommen. Es scheint fast ein Naturgesetz zu sein, dass Software vor Fehlern strotzt.
Das muss aber nicht so sein: es gibt auch fehlerfreie Software. Es ist sogar möglich, für (korrekte) Computerprogramme zu beweisen, dass sie korrekt sind. Man kann mit derselben Präzision, mit der man zeigen kann, dass beispielsweise (\forall x (f(f(x)) = f(x))) \to \exists x(f(x) = x) eine Tautologie ist, ebenfalls beweisen, dass ein bestimmtes Programm immer die Fakultät einer Zahl berechnet. Die in diesem Kapitel vorgestellte Hoare-Logik ist eine möglich Logik, in der man formal zeigen kann, dass Programme korrekt sind. An die Beweise stellen wir dabei genauso hohe Anforderungen wie in der Aussagen- und Prädikatenlogik: Jeder einzelne Beweisschritt muss sehr einfach verifizierbar sein.
Wenn diese Logik so mächtig ist, wieso gibt es überhaupt noch fehlerhafte Software? Wieso wird überhaupt Software ausgeliefert, deren Korrektheit nicht gezeigt wurde? Leider hat sich herausgestellt, dass das Beweisen der Korrektheit von Programmen ein mühseliges Geschäft ist. Genauso, wie es sehr fummelig ist, einen Beweis im Hilbert-Kalkül für eine Formel wie (\forall x (f(f(x)) = f(x))) \to \exists x(f(x) = x) zu führen, ist es anstrengend, für ein etwas längeres Programm (sagen wir, ein zwei Seiten langes) einen Korrektheitsbeweis im Hoare-Kalkül zu führen.
Trotz aller praktischer Widrigkeiten beim Führen von Beweisen im Hoare-Kalkül ist es aber doch ermutigend, dass es prinzipiell möglich ist, beweisbar fehlerfreie Software herzustellen.