Warum korrekte Software zu schreiben so schwer ist – und Mathematik allein nicht hilft
Why Writing Correct Software Is Hard
Der Autor erklärt anhand von Ergebnissen aus Berechenbarkeitstheorie und Komplexitätstheorie, warum Programme und vollständiges Verständnis – die Voraussetzung für Korrektheit – grundsätzlich im Widerspruch stehen. Der Halting-Satz, Rice’s Theorem und der Busy Beaver zeigen: Die Schwierigkeit, Programme zu verifizieren, ist nicht bloß praktisch, sondern eine natürliche Grenze der Berechnung. Selbst kleine Programme von wenigen hundert Zeilen können unentscheidbar sein, wie eine Turing-Maschine mit 1919 Zuständen beweist, deren Terminierung unabhängig von ZFC ist.
Für den Mathematiker gibt es kein Ignorabimus, und meiner Meinung nach auch für die Naturwissenschaft überhaupt nicht. … Der wahre Grund, warum es niemandem gelungen ist, ein unlösbares Problem zu finden, ist meiner Meinung nach der, dass es kein unlösbares Problem gibt.
- turbobutton
Ich glaube, es gibt einen harten Unterschied zwischen abstrakter, mathematischer Korrektheit in Software und dem Funktionieren in der realen Welt. Jede Software, die Eingaben verarbeitet und Menschen komplexe Arbeitsabläufe bietet, muss sich zwangsläufig mit den endlosen Unwägbarkeiten der Realität auseinandersetzen.
Das soll nicht heißen, dass formale Korrektheit keinen Wert hat, aber der wichtige Teil ist zu erkennen, wann sie nützlich ist und wann sie mehr Ärger macht als sie wert ist...
- mpweiher
Ich denke, man muss zuerst herausfinden, was "korrekt" überhaupt ist.
Korrekt in Bezug auf eine formale Spezifikation?
Woher wissen wir, dass die Spezifikation "korrekt" ist? Per Definition?
- johnbender
Soweit ich das beurteilen kann, verwechselt der Artikel fälschlicherweise den Satz von Rice mit der Idee, dass man nichts über das kleine Programm beweisen kann, das von Yedidiya und Aaronson generiert wurde, aber das ist nicht, was der Satz von Rice uns sagt. Stattdessen sagt er uns, dass wir keine allgemeine Methode finden können, um für alle Programme korrekt ja oder nein zu bestimmen, ob ein Programm einen bestimmten Punkt erreicht.
Für ein gegebenes Programm und einen einmaligen Beweis kann man vieles beweisen, oder wenn wir durch die Annahme, dass Schleifen terminieren, überapproximieren, können wir vieles solide beweisen, mit dem Risiko, Programme abzulehnen, die manchmal korrekt sind (z. B. Typsysteme).
Dies könnte jedoch eine Eigenart der Sprache oder meiner Interpretation gewesen sein.
- kodoman
Ich war schon immer an formaler Verifikation interessiert, habe aber nur Spielzeugbeweise geschrieben und Programme abgeleitet.
Es ist schön, diese ältere Diskussion des Themas außerhalb von 'AI does lean' und den Annahmen zu sehen, dass formale Verifikation einfach ist oder für KI einfach sein wird und man einfach sein Gehirn ausschalten kann.
Programme zu bauen, die überhaupt verifiziert werden können, ist ein schwieriges Designproblem, das echtes Nachdenken und tiefe Einsicht in das Problem erfordert.
- tromp
> eine Turingmaschine mit 1919 Kontrollzuständen, von der nicht bewiesen werden kann, dass sie terminiert (d. h. sie ist "unabhängig von ZFC"). Diese Maschine ist so klein, dass sie bequem in eine 4K-Challenge passt
Eine kleine Spitzfindigkeit:
Eine 4K-Challenge bezieht sich normalerweise auf Code, der in 4KB passt, aber eine einfache Kodierung einer TM mit 1919 Zuständen benötigt 19192(2+11) = 49894 Bits oder 6237 Bytes, über 6KB.
Neuere KI-gestützte Optimierungen haben die Anzahl jedoch auf höchstens 215 Zustände gesenkt, was bequem in 1KB passt...
- nirinor
Der wichtigste Teil einer negativen Behauptung ist implizit: Welche vernünftigen Annahmen könnten die Behauptung widerlegen?
Sicher, nach dem Satz von Rice kann kein Programm entscheiden, ob eine beliebige Funktion immer die Summe ihrer beiden Eingaben berechnet. Aber das liegt nur daran, dass wir beliebig schwer zu analysierende Implementierungen der Summenfunktion zulassen. Dieser Satz koexistiert also mit der Tatsache, dass einfache Implementierungen von Summe als korrekt bewiesen werden können.
In diesem Licht denke ich, dass die beste Schlussfolgerung lautet: "Um in angemessener Zeit korrekte Software zu schreiben, müssen wir leicht zu analysierende Sprachen und Programmierstile verwenden".
- bluGill
Die eigentliche Frage ist: Für ein typisches Programm – können wir es beweisen, obwohl wir wissen, dass es Programme gibt, die wir nicht beweisen können?
Die gegebenen Beispiele interessieren mich nicht, ich interessiere mich für meinen Textverarbeitungsprozessor, meinen Webbrowser und ähnliches. Können wir sie beweisen – mit Einschränkungen für die Skriptsprache?
- myrmidon
Ich fand es interessant, wie die untere Schranke für den BB(6)-Champion (2-Symbol-6-Zustand-Busy-Beaver) den Artikel datiert: Er gibt >10^36534 an, aber der aktuelle Champion (mxdys 2025) ist >10↑↑10↑↑10↑↑8 (10↑↑8 ist ein Potenzturm 10^10^10^10... acht hoch, und der Ausdruck wird von rechts nach links aufgelöst, also ist 10↑↑10↑↑8 bereits völlig unvorstellbar groß).