{"id":374,"date":"2025-03-30T13:02:34","date_gmt":"2025-03-30T13:02:34","guid":{"rendered":"https:\/\/philosophy-and-ai.cs.rptu.de\/?page_id=374"},"modified":"2025-07-09T14:32:51","modified_gmt":"2025-07-09T14:32:51","slug":"the-limits-of-correctness","status":"publish","type":"page","link":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/the-limits-of-correctness\/","title":{"rendered":"&#8222;The Limits of Correctness&#8220;"},"content":{"rendered":"\n<p><strong>Brian Cantwell Smith &#8211; 1985<\/strong><br>Am 5. Oktober 1960 meldete die amerikanische Fr\u00fchwarnstation f\u00fcr ballistische Raketen in Thule, Gr\u00f6nland, eine gro\u00dfe Anzahl sowjetischer Raketen, die auf die Vereinigten Staaten zusteuerten. Gl\u00fccklicherweise behielt man bei der unmittelbar einberufenen informellen Bedrohungsanalyse einen k\u00fchlen 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 \u00e4u\u00dferst unwahrscheinlich. Daher wurde kein verheerender Gegenangriff gestartet. Was war das Problem? Der Mond war aufgegangen und reflektierte Radarsignale zur\u00fcck zur Erde. Selbstverst\u00e4ndlich 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 \u201eProgram Verification\u201c investiert \u2013 ein Zweig der Informatik, der sich damit besch\u00e4ftigt, Programme mathematisch auf ihre Korrektheit zu \u00fcberpr\u00fcfen. Die Theorie der Programmkontrolle wurde bereits seit den 1960er Jahren in akademischen Computwissenschafts-Abteilungen erforscht, doch erst in j\u00fcngster Zeit hat sie an \u00f6ffentlicher 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 \u2013 denn selbst ein einziger schwerwiegender Fehler k\u00f6nnte die Gewinnmarge erheblich schm\u00e4lern. W\u00e4hrend es fr\u00fcher nur m\u00f6glich war, die Korrektheit einfachster Programme zu beweisen \u2013 etwa solche, die einfache Listen sortieren oder mathematische Funktionen berechnen \u2013 hat es langsam, aber stetig Fortschritte gegeben, die den Anwendungsbereich dieser Techniken erweitern. Neuere Ver\u00f6ffentlichungen berichten von Korrektheitsbeweisen f\u00fcr 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?<br>(Eigene \u00dcbersetzung des Abstracts <a href=\"https:\/\/www.semanticscholar.org\/paper\/The-limits-of-correctness-Smith\/be8e899bd454aeed7cb4cd67c9b203c954bbf39d\">Semantic Scholar<\/a>)<br><br>DOI: <a href=\"https:\/\/doi.org\/10.1145\/379486.379512\">https:\/\/doi.org\/10.1145\/379486.379512<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Brian Cantwell Smith &#8211; 1985Am 5. Oktober 1960 meldete die amerikanische Fr\u00fchwarnstation f\u00fcr ballistische Raketen in Thule, Gr\u00f6nland, eine gro\u00dfe Anzahl sowjetischer Raketen, die auf die Vereinigten Staaten zusteuerten. Gl\u00fccklicherweise behielt man bei der unmittelbar einberufenen informellen Bedrohungsanalyse einen k\u00fchlen Kopf. Die internationalen Spannungen waren zu diesem Zeitpunkt nicht besonders hoch, das System war erst [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-374","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/pages\/374","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/comments?post=374"}],"version-history":[{"count":2,"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/pages\/374\/revisions"}],"predecessor-version":[{"id":644,"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/pages\/374\/revisions\/644"}],"wp:attachment":[{"href":"https:\/\/philosophie-und-ki.cs.rptu.de\/index.php\/wp-json\/wp\/v2\/media?parent=374"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}