Ihr entwickelt Software, bei der es wirklich darauf ankommt, dass sie korrekt funktioniert? Ob im Medizinbereich, in sicherheitskritischen Systemen oder einfach nur in Code, auf den sich andere verlassen können – dann solltet ihr euch unbedingt mit formalen Methoden beschäftigen. In einer kürzlich veröffentlichten Live-Coding-Session von Never Code Alone zeigt Mike Sperber, Chef der Active Group aus Tübingen, eindrucksvoll, wie man Software nicht nur testet, sondern mathematisch beweist, dass sie tut, was sie soll.
Programmieren durch Basteln vs. Programmieren durch Konstruktion
Mike beginnt mit einer klaren Unterscheidung: Viele von uns programmieren im Modus der „Bastelstunde“ – wir schreiben Code, probieren ihn aus, fügen if-Abfragen hinzu, wenn etwas nicht klappt, und hoffen, dass es irgendwann stabil läuft. Das mag für viele Webanwendungen ausreichen. Aber sobald es um Korrektheit, Sicherheit oder Lebenswichtigkeit geht, reicht das nicht mehr.
Stattdessen plädiert er für Programmieren durch Konstruktion: eine systematische Herangehensweise, bei der jede Funktion von Anfang an so entworfen wird, dass sie gar nicht falsch laufen kann. Und hier kommen formale Methoden ins Spiel.
Warum funktionale Programmierung anders denkt
Ein zentraler Punkt: In funktionalen Sprachen gibt es oft kein if ohne else. Warum? Weil jede Funktion für jeden möglichen Input einen definierten Output liefern muss. Es geht nicht darum, „etwas passieren zu lassen“, sondern darum, klare mathematische Beziehungen zwischen Input und Output herzustellen. Das reduziert Komplexität radikal – und macht Code vorhersagbarer.
Das ist auch der Grund, warum Tests allein oft nicht genug sind: Sie prüfen nur Beispiele, nicht alle möglichen Fälle. Wie beim berühmten Absturz der Ariane-5-Rakete: Der Fehler trat in einem Betriebsmodus auf, der nie getestet wurde – weil niemand daran gedacht hatte.
Spezifikation statt Beispiel: „Für alle“ statt „für diesen Fall“
Der entscheidende Shift: Statt zu sagen „Für diesen Input erwarte ich diesen Output“, sagt eine echte Spezifikation:
„Für alle Inputs gilt: …“
Genau hier setzt die Mathematik an. Mit Quantoren wie ∀ („für alle“) und präzisen Gleichungen beschreibt man das gewünschte Verhalten vollständig – nicht exemplarisch. Das klingt abstrakt, ist aber mächtig: Plötzlich kann man beweisen, dass ein Algorithmus unter allen Umständen korrekt arbeitet.
Praxisbeispiel: Der Bresenham-Algorithmus als Herzschrittmacher
Mike demonstriert das am Bresenham-Algorithmus – ursprünglich entwickelt, um effizient Linien auf Pixel-Displays zu zeichnen. Doch er überträgt ihn clever auf ein Herzschrittmacher-Szenario: Wie verteilt man zusätzliche Herzschläge gleichmäßig, ohne teure Divisionen oder Multiplikationen (wichtig bei batteriebetriebenen Geräten)?
Mit dem Tool Forge modelliert er den Algorithmus deklarativ: nicht als Schritt-für-Schritt-Anweisung, sondern als Menge von logischen Beziehungen. Dann stellt er zwei zentrale Anforderungen als Spezifikation auf:
- Frequenz: Die Zielanzahl an Impulsen wird erreicht.
- Verteilung: Die Impulse liegen gleichmäßig entlang der idealen Linie.
Forge sucht dann automatisch nach Gegenbeispielen – also Fällen, in denen die Spezifikation verletzt wird. Ergebnis: „unsatisfiable“ – kein Gegenbeispiel gefunden (innerhalb des getesteten Bereichs). Das ist keine Hoffnung, sondern eine garantierte Korrektheit für den untersuchten Raum.
Beweis statt Test: Isabelle/HOL und Merge Sort
Noch weiter geht es mit Isabelle/HOL, einem interaktiven Theorembeweiser aus München. Hier wird nicht nur geprüft, sondern mathematisch bewiesen, dass eine Implementierung korrekt ist – für alle möglichen Eingaben, nicht nur für einige.
Am Beispiel von Merge Sort zeigt Mike, wie man Schritt für Schritt nachweist:
- Die Funktion liefert immer eine sortierte Liste.
- Und (implizit): Sie ist eine Permutation der Eingabe – sonst könnte eine triviale Lösung wie „gib immer die leere Liste zurück“ als „korrekt“ gelten.
Der Beweis nutzt Induktion – eine klassische mathematische Technik – und wird vom Tool unterstützt. Das Ergebnis? Absolute Gewissheit. Kein grüner Test, der vielleicht nur Glück hatte. Sondern ein formaler Beweis.
Warum das für euch relevant ist – auch ohne Raketen zu bauen
Vielleicht baut ihr keine Herzschrittmacher oder Flugzeugsteuerungen. Aber:
- Habt ihr komplexe Geschäftslogik (z. B. Steuerberechnung)?
- Müssen eure Systeme DSGVO-konform, sicher oder auditierbar sein?
- Wollt ihr weniger Debugging, weniger Regression und mehr Vertrauen in euren Code?
Dann lohnt sich der Blick auf formale Methoden. Selbst die Art, wie ihr Anforderungen formuliert, wird klarer: Statt QC-Dokumente mit drei Beispielen schreibt ihr Spezifikationen mit „für alle“ – und sprecht damit dieselbe Sprache wie eure Fachabteilung.
Wo geht es weiter?
Interessiert? Mike und sein Kollege Lars Hupel haben ein Advanced-Modul zu formalen Methoden im ISAQB entwickelt – erste Schulungen starten im zweiten Halbjahr 2026. Außerdem lohnt sich ein Besuch der BOB-Konferenz am 13. März in Berlin, wo gleich mehrere Talks zu formalen Methoden stattfinden.
Und Tools wie Forge, Isabelle/HOL oder Lean 4 sind frei verfügbar – perfekt, um selbst zu experimentieren.
Fazit: Korrektheit ist kein Luxus – sondern eine Haltung
Formale Methoden sind kein akademischer Elfenbeinturm. Sie sind ein praktisches Werkzeug, um Software zu bauen, die wirklich funktioniert – nicht nur meistens, sondern immer. In einer Welt, in der Software unser Leben steuert, ist das keine Option, sondern eine Verantwortung.
Ihr wollt tiefer einsteigen?
Meldet euch gerne bei uns – wir unterstützen euch bei der Integration formaler Methoden in eure Projekte, bei Schulungen oder bei der Auswahl der richtigen Tools. Denn am Ende geht es nicht darum, möglichst viel Code zu schreiben – sondern darum, den richtigen Code zu schreiben. Und dafür gibt es jetzt endlich bessere Wege als nur Tests.
