Wie man durch kleine Beweise im Kopf ein besserer Programmierer wird

• Um ein besserer Programmierer zu werden, ist es wichtig, sich beim Schreiben von Code die Gewohnheit anzueignen, kleine Beweise im Kopf zu skizzieren
• Monotonie, Unveränderlichkeit, Vor- und Nachbedingungen sowie Invarianten sind dabei zentrale Konzepte für solche Mini-Beweise
• Beim Entwurf hilft es enorm, den Einflussbereich von Codeänderungen auf das Gesamtsystem zu berücksichtigen (Isolation, Firewall), um Komplexität und Risiken zu verringern
• Mit Induktion lässt sich die Korrektheit rekursiver Funktionen oder Strukturen schrittweise beweisen
• Diese Denkweise wird durch Übung und Gewohnheit verankert; tatsächliche mathematische Beweise und das Lösen von Algorithmusaufgaben helfen dabei sehr

---

Einführung und Kerngedanke

• Der Autor hat sich mit wachsender Berufserfahrung ganz natürlich die Gewohnheit angeeignet, kleine Beweise zu skizzieren, um die Korrektheit und Geschwindigkeit seines Codes zu verbessern
• Der Prozess, während des Codens das erwartete Verhalten im Kopf zu überprüfen und herzuleiten, erfordert Übung; mit zunehmender Sicherheit steigt die Qualität des Codes jedoch spürbar
• Entscheidend ist nicht, wie genau man das tut; man kann es auf unterschiedliche Weise üben und den für sich passenden Ansatz finden

Monotonie (Monotonicity)

• Monotonie (monotonicity) bezeichnet die Eigenschaft, dass eine Funktion oder ein Stück Code sich nur in eine Richtung bewegt
• Als Beispiel wird Checkpointing genannt: Der Arbeitsfortschritt bewegt sich nur vorwärts, und bereits erledigte Arbeit wird nicht wieder zurückgerollt und erneut ausgeführt
• Im Beispiel LSM-Tree im Vergleich zum B-Tree sammelt sich beim LSM-Tree der Speicherverbrauch meist an und nimmt nur während der Kompaktierung wieder ab
• Wenn Monotonie garantiert ist, lassen sich bestimmte komplexe Zustände oder Teile möglicher Ergebnisse auf natürliche Weise ausschließen oder vorhersagen
• Unveränderlichkeit (immutability) ist ein ähnliches Konzept: Ein einmal gesetzter Wert ändert sich nie, sodass mögliche Zustandsänderungen ausgeschlossen werden können

Vor- und Nachbedingungen (Pre- and post-conditions)

• Vorbedingungen (pre-condition) und Nachbedingungen (post-condition) sind Aussagen, die vor beziehungsweise nach der Ausführung einer Funktion zwingend wahr sein müssen
• Wenn man diese Bedingungen beim Schreiben einer Funktion explizit mitverfolgt, hilft das beim logischen Denken und beim Testen
• Sind Nachbedingungen klar definiert, lassen sich Unit-Test-Fälle leichter ableiten
• Das Hinzufügen von Assertions im Code, die diese Bedingungen prüfen und bei unerwarteten Situationen frühzeitig abbrechen, erhöht Vorhersagbarkeit und Sicherheit
• Mitunter ist es schwer, einer Funktion überhaupt klare Vor- oder Nachbedingungen zu geben; schon diese Erkenntnis ist aufschlussreich

Invarianten

• Invarianten sind Eigenschaften, die in jeder Situation, also vor, während und nach der Ausführung, immer wahr sein müssen
• Ein typisches Beispiel ist die Bilanzgleichung der doppelten Buchführung (Summe Haben = Summe Soll)
• Wenn man den gesamten Code in kleine Schritte zerlegt und beweist, dass jeder Schritt die Invarianten erhält, kann man die Integrität des Gesamtsystems sicherstellen
• Um Invarianten zu erhalten, kann man etwa Listener oder Lifecycle-Methoden verwenden (zum Beispiel Konstruktoren/Destruktoren in C++ oder useEffect in React)
• Je weniger Änderungen es gibt oder je einfacher die Pfade sind, desto leichter lässt sich die Gültigkeit von Invarianten prüfen

Isolation

• Eines der Kernelemente guter Software ist, neue Funktionen hinzuzufügen oder Änderungen vorzunehmen, ohne das bestehende System instabil zu machen
• Man muss den „blast radius“ von Codeänderungen verstehen und strukturelle „Firewalls“ schaffen, um die Ausbreitung von Auswirkungen zu minimieren
• Am Beispiel des realen Dienstes Nerve wird gezeigt, wie man die Grenze zwischen Query Planner und Query Executor klar definiert und so entwirft, dass Änderungen diese Grenze nicht überschreiten
• Verhindert man unnötige Ausbreitung von Änderungen, werden Verifikation und Wartung einfacher und die Stabilität steigt
• Das entspricht auch der Philosophie des OCP (Open-Closed Principle): Funktionen erweitern, ohne bestehendes Verhalten zu verändern

Induktion

• Viele Programme enthalten rekursive Funktionen oder rekursive Strukturen, und Induktion ist ein mächtiges Mittel, um dafür eine saubere Logik aufzubauen
• Um das Verhalten und die Korrektheit rekursiver Funktionen schrittweise zu beweisen, müssen Basisfall (base case) und Induktionsschritt (inductive step) jeweils überprüft werden
• Als Beispiel dient der Vereinfachungsprozess von Knoten in einer AST-Struktur; durch induktive Argumentation für jeden Schritt werden das Erhalten von Invarianten und korrektes Verhalten bewiesen
• Wenn sich induktives Denken verinnerlicht, wird das Schreiben und Verifizieren rekursiven Codes deutlich intuitiver und einfacher
• Im Vergleich zu nicht-induktiven, globalen (holistischen) Verifikationsversuchen lässt sich darüber nachdenken, welcher Ansatz natürlicher ist

Proof-affinity als Qualitätsmaß

• Der Autor vertritt die These, dass Code gut ist, wenn man dafür kleine Beweise im Kopf skizzieren kann
• Wenn Code Strukturen wie Monotonie, Unveränderlichkeit, klare Bedingungen, aufgeteilte Invarianten, Firewall-Grenzen und den Einsatz von Induktion besitzt, wird er tatsächlich leichter beweisbar und damit qualitativ besser
• Ist Code schwer zu verstehen und schwer zu verifizieren, deutet das darauf hin, dass Refactoring oder ein strukturelles Umdenken nötig ist
• Statt von „Beweisbarkeit“ spricht der Autor hier lieber von „proof-affinity“
• Proof-affinity ist nicht der einzige Faktor für Softwarequalität, aber ein sehr wichtiger Verstärker für Verständnis, Erweiterbarkeit, Tests und Wartung von Code

Wie man besser wird

• Diese Art logischen Denkens wird erst durch Übung so verinnerlicht, dass sie unbewusst und natürlich angewendet wird
• Es ist unverzichtbar, regelmäßig (mathematische) Beweise zu formulieren und die Fähigkeit zum logischen Schlussfolgern zu trainieren
• Auch das Lösen von Algorithmusaufgaben (Stanford-EdX-Kurse, Leetcode usw.) ist ein gutes Übungsfeld; besonders hilfreich sind Aufgaben, die nicht nur Tricks, sondern sorgfältige Implementierung und beweisartiges Denken erfordern
• Wichtig ist, nicht durch wiederholtes Nachbessern irgendwie zum richtigen Ergebnis zu kommen, sondern zu üben, sich ihm möglichst gleich beim ersten Versuch stark anzunähern
• Durch diese Gewohnheitsbildung verbessern sich logischer Systementwurf und Codequalität erheblich

[GN⁺]

Hacker-News-Kommentare

• Es gibt ein perfektes, simples und zugleich erstaunliches Beispiel, das genau zu diesem Thema passt: die binäre Suche. Es gibt Varianten für links und rechts, aber wenn man nicht über Schleifeninvarianten nachdenkt, ist es sehr schwer, sie korrekt zu implementieren. Dieser Artikel erklärt den Invarianten-Ansatz und zeigt dazu passenden Python-Code. Jon Bentley, der Autor von Programming Pearls, ließ IBM-Programmierer eine gewöhnliche binäre Suche implementieren, und 90 % davon enthielten Bugs. Meist waren es Fehler, die zu Endlosschleifen führten. Damals musste man sich auch noch selbst gegen Integer-Overflow absichern, daher ist das in gewisser Weise nachvollziehbar, aber die Quote ist trotzdem erstaunlich

  • Nachdem ich das gesehen hatte, fing ich an, binäre Suche als Interviewfrage zu verwenden. Etwa zwei Drittel der eigentlich starken Kandidaten konnten innerhalb von 20 Minuten keine korrekt funktionierende Implementierung schreiben. Besonders häufig landeten sie schon in einfachen Fällen in einer Endlosschleife. Wer erfolgreich war, implementierte sie schnell. Eine Ursache ist wohl, dass viele mit einer falschen Schnittstelle gelernt haben. Selbst Wikipedia erklärt es als „Initialisiere L mit 0 und R mit n-1“, also mit einem Bereich, in dem R enthalten ist. In der Praxis ist aber in den meisten String-Algorithmen eine obere Grenze ohne Einschluss, also R = n, besser. Ich würde diese Hypothese gern direkt testen. Man müsste viele Leute mit unterschiedlichen Funktionsprototypen und Initialwerten arbeiten lassen und dann vergleichen, wie viele Bugs bei inklusiver oder exklusiver oberer Grenze oder bei einer Längen-basierten Variante auftreten

  • Tatsächlich ist die binäre Suche fast das Paradebeispiel dafür, wie knifflig Indexverwaltung sein kann. Zusammen mit Hoares Partitionierungsalgorithmus gehört sie zu den grundlegenden Algorithmen, die sich am schwersten fehlerfrei und exakt codieren lassen

  • Zum Test habe ich Claude Sonnet gebeten, fehlerfreien Python-Code für die binäre Suche zu schreiben

  def binary_search(arr, target):
      left = 0
      right = len(arr) - 1
      while left <= right:
          mid = left + (right - left) // 2
          if arr[mid] == target:
              return mid
          elif arr[mid] < target:
              left = mid + 1
          else:
              right = mid - 1
      return -1
  

  Ich habe auch verschiedene Testfälle mit Beispiel-Arrays überprüft

  • Weil bekannt ist, dass Bugs bei der binären Suche ein berüchtigtes Anti-Beispiel sind, wollte ich die erste fehlerfreie Implementierung in ein Buch aufnehmen. Ich habe sie wirklich vorsichtig geschrieben, und trotzdem war ein Bug drin, was im Nachhinein ziemlich komisch ist. Zum Glück konnte ich ihn dank Mannings Vorab-Feedback-System vor dem Druck noch korrigieren

  • Ich implementiere linke/rechte binäre Suche immer so, dass ich mir den „bisher besten Wert“ merke. Ähnlich wie lower_bound und upper_bound in C++. In einer while (l < r)-Struktur finde ich den Mittelpunkt, prüfe die aktuelle Position und passe dann den Bereich passend an. Bei upper_bound verschiebe ich zum Beispiel die linke Grenze nach oben, bei lower_bound senke ich die rechte Grenze. Ich habe seit Längerem wieder Leetcode gelöst und war etwas benebelt, daher ist das Format vielleicht chaotisch

• Ich glaube, ich bin schon vor langer Zeit in einem Graduiertenkurs auf ein ähnliches Konzept gestoßen. Gegen Ende meines Bachelorstudiums habe ich Mathematikprüfungen nur noch mit Kugelschreiber geschrieben. Ich wusste nicht genau warum, aber meine Noten waren konstant hoch, weil ich die Aufgaben in einem Zug löste und den gesamten Lösungsweg vorher vollständig im Kopf durchging. Dadurch machte ich viel weniger Fehler. Beim Programmieren gehe ich ähnlich vor und entwerfe die Lösung im Kopf möglichst vollständig, bevor ich beginne

• Um ein besserer Programmierer zu werden, sollte man sich angewöhnen, kleine Beweise zum Code zu schreiben Tests und Typdefinitionen sind genau solche Handlungen Ich gehe dabei besonders oft in der Reihenfolge vor: zuerst Tests, dann Typen, zuletzt der Code Für jedes einzelne Acceptance Criterion sollte man Tests anlegen, und idealerweise sollten diese Tests Ein- und Ausgabe klar beschreiben Bei APIs kann man mit OpenAPI oder GraphQL zuerst eine Spezifikation mit allen Eigenschaften und Typen erstellen. Zur Laufzeit kann man Daten anhand dieser Spezifikation validieren, und die Spezifikation selbst wird zum Beleg dafür, dass die Anwendung gemäß Spezifikation funktioniert Kurz gesagt ist es wichtig, sich über OpenAPI/GraphQL, Tests und Typen einen Nachweis zu verschaffen, dass das System tatsächlich wie beabsichtigt funktioniert Wenn die Spezifikation selbst zuerst gut entworfen ist, kann man die Code-Implementierung flexibel ändern und die Korrektheit trotzdem über die Spezifikation nachweisen Die Spezifikation ist wichtiger als der Code selbst

  • Die fünf im Artikel genannten Eigenschaften lassen sich in guten Typsystemen ausdrücken. Auf diese Weise wird ein großer Teil der Spezifikation selbst zu Code, und der Compiler garantiert die Korrektheit. Die Zukunft des Programmierens sollte in diese Richtung gehen, sodass dieser Ansatz selbstverständlich wird OpenAPI und die Typsysteme von GraphQL sind viel zu schwach; bis wir diese Zukunft erreichen, brauchen wir wohl noch 50 Jahre Entwicklung

• Ich habe an der Universität die Grundlagen der theoretischen Informatik gelernt und kann dem Anliegen des Artikels zustimmen. In der Praxis ist das allerdings nicht leicht Neben Vor- und Nachbedingungen sind auch CS-Beweistechniken wie Schleifeninvarianten (loop invariant) und strukturelle Induktion (structural induction) sehr mächtig Zusammen mit den Links zu loop invariant und structural induction empfehle ich die Vorlesungsunterlagen von UofT CSC236H (Vorlesungsunterlagen)

  • Diese CSC236-Unterlagen sind wirklich hervorragend, und Professor David Liu ist auch ein wirklich guter Mensch Professorenprofil

  • UofT wurde erwähnt! Freut mich irgendwie

• Die Aussage „im Kopf kleine Beweise über den Code selbst konstruieren“ ist ein so wichtiges Prinzip, dass sie eigentlich selbstverständlich sein sollte. Man sollte sich immer einer einfachen Aussage darüber bewusst sein, was jeder Teil des Codes tut

  • In Greenfield-Projekten (vor allem, wenn man den gesamten Code selbst geschrieben hat) ist das leicht, aber in echten Codebasen, in denen viele Entwickler an verschiedenen Funktionen oder globalem Zustand arbeiten, fühlt es sich deutlich schwerer an

    • Wirklich gute Entwickler haben die Fähigkeit, ein System schrittweise in diese Richtung weiterzuentwickeln. Echter Code ist chaotisch, aber wichtig ist, die Lücken in den Invarianten nach und nach zu schließen und eine Code-Struktur zu schaffen, in der auch nachfolgende Entwickler die Invarianten erkennen und eher erhalten als zerstören. Dokumentation hilft, aber meiner Erfahrung nach spielt die Code-Struktur selbst eine noch größere Rolle

    • Genau das ist eigentlich der entscheidende Grund, warum globaler Zustand gefährlich ist. Um die Korrektheit des Codes zu beweisen, muss man dann das gesamte Programm kennen. Wenn man globale Variablen in unveränderliche Werte umwandelt, sie als Funktionsargumente übergibt oder den Zustand in einer Wrapper-Klasse kapselt, muss man nur noch die Aufrufer dieser Funktion klar überblicken. Wenn man im Funktionsinneren zusätzlich Constraints etwa über Assertions einführt, wird der Beweis deutlich einfacher. Viele Programmierer treffen solche Entscheidungen bereits, nur oft instinktiv und nicht mit dem Bewusstsein, gerade Beweisbarkeit zu fördern

    • Code, in dem mehrere Entwickler globalen Zustand verwalten, lässt sich mit einem Patienten vergleichen, bei dem „der Krebs metastasiert hat“. Die Behandlung ist viel schwieriger, und manchmal lässt sich so etwas nur mit Glück und günstigen äußeren Umständen noch retten

    • Wie im Artikel gesagt, ist bei solcher Art von Code die Wahrscheinlichkeit von Bugs viel höher, und auch das Risiko zusätzlicher Bugs durch Wartung steigt stark. Das zeigt, dass es deutlich richtiger ist, von Anfang an eine beweisbare Struktur anzustreben

    • Dieser Artikel erinnert mich daran, dass ich meine Art zu programmieren ständig neu hinterfrage und versuche, mich in eine bessere Richtung auszurichten. Ich frage mich, ob selbst Entwickler wie John Carmack mit der Zeit auf ihren früheren Code zurückblicken und ihn als unzureichend empfinden und ein Gefühl dafür haben, immer „besser“ zu werden

• Die Idee, dass Code beweisbar sein sollte, wurde erstmals sichtbar, als Dekker 1959 das Mutual-Exclusion-Problem löste. Eine interessante Anekdote dazu findet sich in Dijkstras Text EWD1303 (Originallink). Auch Dijkstras spätere Arbeiten kann man als Fortsetzung dieser Einsicht sehen

• Einen korrekten Beweis zu schreiben ist wirklich schwer. Programmverifikation ist ebenso nicht einfach. Meiner Meinung nach ist es ineffizient, Beweise von Hand schreiben zu wollen. Wenn man idiomatischen Code schreibt, der zur Sprache und zur Codebasis passt, muss man sich kaum um Invarianten oder Vor- und Nachbedingungen kümmern. Das in „The Practice of Programming“ von R. Pike und B. W. Kernighan betonte Prinzip von „Einfachheit, Klarheit und Allgemeingültigkeit“ hat in der Praxis eine enorme Wirkung. Etwas verwandt, aber doch ein anderes Thema: Wer Competitive Programming macht, merkt schnell, dass man Techniken zur Sicherstellung der Korrektheit des Codes wirklich beherrschen muss, um auf das nächste Niveau zu kommen

  • Dem kann ich nicht zustimmen. Ich glaube nicht, dass der Autor des Artikels vollständige formale Beweise meint, sondern dass man sich unbedingt Gedanken darüber machen sollte, welche logischen Eigenschaften der eigene Code garantiert, zum Beispiel Invarianten. Das ist der beste Weg, den Code zu verstehen und die Angst vor seinem Inhalt loszuwerden

  • Hier scheinen Ursache und Wirkung eher vertauscht zu sein. Wenn man ein Problem sorgfältig durchdenkt, wird der resultierende Code ganz natürlich klar und sauber. Eine klare Logik führt zu einem klaren Code-Design. Aber zu glauben, sauber geschriebener Code bringe von sich aus Korrektheit mit, ist Unsinn. Natürlich hilft sauberer Code dabei, Bugs bei Code-Reviews und Ähnlichem zu verringern. Man sollte nur im Kopf behalten, dass die Form der Funktion folgt

  • Das grundlegendste Konzept eines Beweises ist „warum das hier richtig ist“. Es geht nicht nur darum, triviale Fehler zu vermeiden, sondern grundlegend zu prüfen, ob die Richtung überhaupt stimmt

  • Für die Korrektheit von Code gibt es keinen Ersatz außer dem richtigen Schreiben des Codes selbst. Auch wenn es schwierig ist: Er muss einfach korrekt geschrieben werden

  • Wenn man den ersten Absatz komplett umdreht, ergibt sich: Mit geeigneten Abstraktionen (also idiomatischem Code passend zu Sprache und Codebasis) wird Programmverifikation leichter. Bei geeigneten Abstraktionen muss man nicht mehr über Schleifeninvarianten und Ähnliches nachdenken, weil aus der Korrektheit des Codes der Beweis direkt folgt

• Veränderlichkeit und Unveränderlichkeit (mutable/immutable) sind ebenfalls wichtige Eigenschaften. Wenn man Zustand möglichst unveränderlich hält, reduziert das nicht nur die Komplexität bei Multithreading, sondern auch beim Nachvollziehen des Programmzustands

  • Das steht im Originalartikel bereits drin

• In den 80ern wurde mir als Undergraduate an Carnegie Mellon dieses Prinzip sehr klar beigebracht. Es hat mir später im Leben enorm geholfen. Besonders die Erkenntnis, dass Rekursion und Induktion äquivalent sind, half mir damals dabei, rekursive Algorithmen nicht mehr als „wild ausprobieren, bis eine Antwort herausfällt“ zu behandeln, sondern sauber anzugehen

  • Ich habe diese Vorlesung vor Kurzem besucht, und im funktionalen Programmieren hatte ich ein noch stärkeres Aha-Erlebnis