Brian Cantwell Smith – 1985
Am 5. Oktober 1960 meldete die amerikanische Frühwarnstation für ballistische Raketen in Thule, Grönland, eine große Anzahl sowjetischer Raketen, die auf die Vereinigten Staaten zusteuerten. Glücklicherweise behielt man bei der unmittelbar einberufenen informellen Bedrohungsanalyse einen kühlen Kopf. Die internationalen Spannungen waren zu diesem Zeitpunkt nicht besonders hoch, das System war erst vor Kurzem installiert worden, Chruschtschow befand sich in New York, und insgesamt erschien ein massiver sowjetischer Angriff äußerst unwahrscheinlich. Daher wurde kein verheerender Gegenangriff gestartet. Was war das Problem? Der Mond war aufgegangen und reflektierte Radarsignale zurück zur Erde. Selbstverständlich hatten die Designer des Systems diese Reflexion nicht vorhergesehen. In den letzten zehn Jahren hat das Verteidigungsministerium viele Millionen Dollar in eine neue Computertechnologie namens „Program Verification“ investiert – ein Zweig der Informatik, der sich damit beschäftigt, Programme mathematisch auf ihre Korrektheit zu überprüfen. Die Theorie der Programmkontrolle wurde bereits seit den 1960er Jahren in akademischen Computwissenschafts-Abteilungen erforscht, doch erst in jüngster Zeit hat sie an öffentlicher Aufmerksamkeit gewonnen und wird zunehmend auf reale Probleme angewendet. General Electric beispielsweise hat eigene Verifikationsprojekte ins Leben gerufen, um sicherzustellen, dass die Programme ihrer neuesten computergesteuerten Waschmaschinen fehlerfrei arbeiten – denn selbst ein einziger schwerwiegender Fehler könnte die Gewinnmarge erheblich schmälern. Während es früher nur möglich war, die Korrektheit einfachster Programme zu beweisen – etwa solche, die einfache Listen sortieren oder mathematische Funktionen berechnen – hat es langsam, aber stetig Fortschritte gegeben, die den Anwendungsbereich dieser Techniken erweitern. Neuere Veröffentlichungen berichten von Korrektheitsbeweisen für etwas komplexere Programme, darunter kleine Betriebssysteme, Compiler und andere essenzielle Komponenten moderner Systemarchitektur. Doch was bedeutet diese neue Technologie wirklich? Wie gut sind wir darin?
(Eigene Übersetzung des Abstracts Semantik Scholar)
DOI: https://doi.org/10.1145/379486.379512