Formale Methoden und die Zukunft des Programmierens

• Formale Methoden sind Werkzeuge, mit denen sich beweisen lässt, ob Software die beabsichtigten Eigenschaften erfüllt; durch die Verbreitung von Agent Coding verschiebt sich die Abwägung von Kosten und Nutzen
• Jane Street war früher der Ansicht, dass formale Methoden – abgesehen von einigen Sonderfällen – im Verhältnis zu den Kosten nur geringen Wert bieten, baut nun aber ein dediziertes Team auf
• Für die Verifikation von 8.700 Zeilen C-Code in seL4 waren 25 Personenjahre nötig; pro Codezeile brauchte es etwa 23 Zeilen Beweis und einen halben Personentag Verifikation
• Zwischen von Agenten erzeugtem Code und releasefähiger Qualität besteht weiterhin eine Lücke; als Mittel, den Verifikationsengpass zu verringern und Agenten starkes Feedback zu geben, werden formale Methoden wichtiger
• Jane Street sieht Spielraum, OxCaml gemeinsam mit beweisorientierten Techniken weiterzuentwickeln, weil das Unternehmen die Sprache tiefgreifend kontrollieren kann und es eine vorbereitete Programmierer-Community gibt

---

Formale Methoden und die Zukunft des Programmierens

• Jane Street hat in den vergangenen 25 Jahren immer wieder gesagt, dass man auf Organisationsebene kein Interesse an formalen Methoden habe, hält diese Position nun aber nicht mehr aufrecht
• Die Stärke von Werkzeugen für besseren und verlässlicheren Code wurde schon lange geschätzt, und Typsysteme galten als leichtgewichtige formale Methode mit großem Nutzen
• Abgesehen von Sonderfällen, insbesondere der Hardware-Synthese, wurde jedoch angenommen, dass formale Methoden zu teuer seien und daher für die meiste Software nicht passten
• seL4 ist ein formal verifizierter Mikrokernel und eine wichtige Leistung, doch für die Verifikation von 8.700 Zeilen C-Code waren 25 Personenjahre nötig
  • Pro Codezeile waren etwa 23 Zeilen Beweis nötig, und die Verifikation einer Zeile erforderte ungefähr einen halben Personentag
• In Fällen mit hohem Risiko und relativ klarer Spezifikation, etwa bei sicherheitskritischen Mikrokernels, kann ein solcher Ansatz wertvoll sein
• Für den Großteil der Software passte er jedoch nicht, und auch für Jane Streets wichtigste Software schien er nicht geeignet
• Das Aufkommen von Agent Coding hat diese Einschätzung verändert, und Skepsis gegenüber dem Potenzial formaler Methoden ist in Erwartung umgeschlagen
• Jane Street stellt ein Team für formale Methoden zusammen und hofft, daraus ein ebenso breit nützliches Werkzeug zum Softwarebau zu machen wie ausgefeilte Typsysteme

Warum sich die Meinung geändert hat

• Agent Coding verändert auf mehrere Arten die bisherige Kosten-Nutzen-Struktur formaler Methoden
• Das bedeutet nicht, dass Agenten beliebig schwierige Beweise allein konstruieren können, aber Modelle leisten große Hilfe und ermöglichen mehr Menschen einen produktiven Einsatz der Werkzeuge
• Da die Nutzung formaler Methoden einfacher wird als früher, lohnt es sich, die frühere Kosten-Nutzen-Rechnung neu zu bewerten

• Der Verifikationsengpass wird wichtiger

  • Modelle werden immer besser darin, nützlichen Code zu schreiben, aber zwischen modellgeneriertem Code und tatsächlich releasefähigem Code liegt weiterhin ein großer Abstand
  • Modelle sind erstaunlich gut darin, ein vorgegebenes Ziel zu erreichen, aber nicht stark genug darin, dabei die Qualität einer Codebasis zu erhalten oder zu verbessern
  • Von Agenten erzeugter Code wird besser, ist aber oft zu komplex, enthält seltsame Bugs und Grenzfälle und neigt dazu, die zentralen Invarianten einer Codebasis nicht einzuhalten
  • Menschen müssen viel Zeit darauf verwenden zu prüfen, ob von Agenten erzeugter Code eine ausreichende Qualität hat
  • Formale Methoden können diese Verifikationslast verringern und den Review-Prozess effizienter machen

• Agenten profitieren stark von Feedback

  • Agenten profitieren sowohl beim Training mit Reinforcement Learning als auch beim Einsatz fürs Programmieren von Feedback
  • Formale Methoden können eine starke Form von Feedback sein, die die Fähigkeit von Agenten verbessert, schwierige Probleme zu lösen
  • Tests bleiben ebenfalls sehr wertvoll und lassen sich mit property-based testing und Fuzzing weiter verbessern
  • Tests allein reichen jedoch nicht aus, und es gibt inhärente Grenzen dabei, den vom Programm erreichbaren Zustandsraum abzudecken
  • Aus der Programmiererfahrung mit OxCaml zeigt sich, dass Agenten stark von den universellen Garantien eines Typsystems profitieren
  • Wenn ein Typsystem Data Races verhindern kann, lassen sich Data Races eliminieren
  • Wenn sich durch gut gestaltete Typen Cross-Site-Scripting-Schwachstellen unmöglich machen lassen, können Schwachstellen auf eine Weise beseitigt werden, die mit bloßem Testen schwer erreichbar ist
  • Typen entschärfen beim Programmieren mit Agenten den Verifikationsengpass und liefern besseres Feedback
  • Mit stärkeren Beweistechniken könnte es zusätzlichen Spielraum für Verbesserungen geben

Warum hier

• Weltweit denken viele darüber nach, was Agenten für die Zukunft des Programmierens bedeuten, und es gibt zahlreiche Startups, die formale Methoden mit Agenten verbinden wollen
• Jane Street kann die verwendete Sprache tiefgreifend kontrollieren und sie deshalb so anpassen, dass sie besser für beweisorientierte Techniken geeignet ist
• Dafür gibt es verschiedene mögliche Richtungen
  • Modulare Spezifikationen von Eigenschaften könnten in das Typsystem integriert werden
  • Beschränkungen auf Typebene für Dinge wie Ownership und Mutability könnten bestimmte Beweise erleichtern
  • Beweistechniken könnten direkt in die Sprache eingebaut werden

• Eine vorbereitete Programmierer-Community

  • Bei Jane Street gibt es eine Programmierer-Community, die bereit ist, solche Techniken anzunehmen
  • Für Menschen, die mit Programmiersprachen arbeiten, ist es oft schwieriger, gute neue Programmierideen tatsächlich im Arbeitsalltag zur Nutzung zu bringen, als sie überhaupt zu entwickeln
  • Bei Jane Street kommt es häufig vor, dass Nutzer unzufrieden sind, weil versprochene neue und ungewohnte Funktionen des Typsystems nicht schnell genug erscheinen
  • Es gibt viele Menschen mit dem nötigen Hintergrund, um solche Techniken zu nutzen, und das Interesse an korrekten Ergebnissen und hochwertiger Software ist bereits fest verankert
  • Eine aktive Nutzerbasis mit hohen Erwartungen gibt die Freiheit, kurzfristige Verbesserungen und langfristige Visionen zugleich zu verfolgen
  • Kurzfristige Verbesserungen können vergleichsweise schnell Wirkung entfalten
  • Langfristige Visionen können ambitioniertere Ziele sein, die sich über mehrere Jahre erreichen lassen
  • Aus kurzfristigen Versuchen lässt sich lernen, während gleichzeitig auf langfristige Ziele hingearbeitet wird

• Beziehung zu externen Tools

  • Die Arbeit außerhalb des Unternehmens wird nicht ignoriert; vielmehr schöpft man Erwartungen und Inspiration aus der Arbeit verschiedener Programmiersprachen-Communities
  • Zu den relevanten Tools gehören Lean, Dafny, Rocq, Agda und Iris
  • Es wird nach Wegen gesucht, OxCaml mit einigen dieser Tools zu integrieren, um bereits vorhandene hervorragende Infrastruktur zu nutzen
  • Zugleich sieht man einzigartige Vorteile, die sich nur realisieren lassen, wenn Sprache und Beweistechniken gemeinsam behandelt werden

Hinweis zum Mitmachen

• Jane Street sucht in London und New York nach Fachkräften für formale Methoden
• Die Interviews und der Teamaufbau für diese Rollen befinden sich derzeit noch in einer frühen Phase
• Es gibt noch sehr viel zu tun, und man sucht Menschen, die zum Team stoßen wollen

Ergänzung

• Modelle brauchen beim Umgang mit komplexen Beweisen weiterhin menschliche Hilfe und Anleitung
• Menschliche Programmierer können Ideen dazu haben, warum ein System funktioniert und wie sich das auf hoher Ebene beweisen lässt
• Die meisten Programmierer wissen jedoch nicht, wie sich eine Beweisidee so kodieren lässt, dass sie ein bestimmtes Beweissystem erfüllt
• Modelle können bei den technischen Details des Beweisschreibens viel repetitive Arbeit automatisieren und Fachwissen einbringen
• Schlupflöcher wie Obj.magic können Beschränkungen auf Typebene umgehen
• Wenn solche Ausnahmen im Großteil des Codes nachverfolgt und verboten werden, lässt sich ein Zustand erreichen, der universellen Garantien sehr nahekommt
• Formale Methoden können explizit machen, warum die Nutzung solcher Schlupflöcher im konkreten Fall tatsächlich sicher ist

[GN⁺]

Hacker-News-Kommentare

• Ich habe vor Jahrzehnten an Korrektheitsbeweisen gearbeitet, und das damalige System hatte mehr Beweisautomatisierung als viele spätere Systeme.
  Die einfachen Teile erledigte der Oppen-Nelson-Simplifier, der erste SAT-Solver, und die schwierigen Teile übernahm der Boyer-Moore-Prover, der Heuristiken und frühere Hilfslemmata nutzte. Die schwierige Aufgabe für Menschen bestand darin, den Prover ausprobieren zu lassen und dann Hilfslemmata vorzuschlagen, die in späteren Beweisen verwendet werden konnten.
  Spätere Systeme scheinen weniger Automatisierung gehabt zu haben, und ich denke, dass formale Methoden ihr Ziel verfehlt haben, weil sie sich zu sehr im Formalismus verloren und zu wenig an der Praxis orientiert waren. Aus Sicht von jemandem, der in kommerziellen Projekten fehlerfreien Code wollte, wirkten akademische Projekte oft von Mathematikern geprägt, die knappe Notation für Papers und eine geringe Fallanalyse bevorzugten.
  In der Praxis braucht man viel automatisiertes Durchackern und sollte nur wenig Einsicht benötigen. Schlaue Leute haben immer wieder neue Logiken wie Modallogik oder Temporallogik erfunden, um die Ausführlichkeit von Papier-und-Bleistift-Beweisen zu vermeiden, aber das hat nicht besonders geholfen. Die grundlegende Wahrheit in diesem Feld ist, dass die meisten Theoreme ziemlich banal sind.
  Wie die Leute bei Jane Street sagen, ist die Sprache kontrollieren zu können ein großer Vorteil. Verifikationsaussagen sollten in die Programmiersprache integriert sein; wenn sie in Kommentaren, anderer Syntax oder separaten Dateien stecken, entsteht nur unnötiger Mehraufwand. Es wirkt sinnvoll, dass Jane Street in diese Richtung drängt.
  Ich war damit vor mehr als 40 Jahren einfach zu früh dran; damals dauerte es mit dem Boyer-Moore-Prover etwa 45 Minuten Rechenzeit, Zahlentheorie von Grund auf aufzubauen, heute dauert das nicht einmal 1 Sekunde.
  https://archive.org/details/manualzilla-id-5928072/page/n3/m...

  • Als jemand, der lange mit formalen Methoden gearbeitet hat, fällt es mir etwas schwer, der Aussage zuzustimmen, dass neue Logiken nicht helfen. Industrielle Logiken sind praktisch und erlauben es, anspruchsvolle Eigenschaften, die ein System erfüllen muss, sehr prägnant auszudrücken.
    Logik hat in der Informatik und im Software Engineering eine ähnliche Stellung wie die Analysis in Physik, Maschinenbau oder Bauingenieurwesen. Dinge wie LTL oder die neuere Separation Logic waren enorme Durchbrüche.
    Die recht große Popularität von TLA+ ist ein Beleg dafür, und Model Checking ist sehr praktisch. Spannend ist heute, dass schwergewichtigere formale Methoden, insbesondere Theorembeweisen, vielleicht günstig genug werden könnten, um auch in allgemeiner Systemsoftware eingesetzt zu werden.
    Formale Spezifikationen für Funktionen zu schreiben und sie mit einer Hybridmethode aus SAT/SMT, Theorembeweisern und LLMs zu synthetisieren und ihre Korrektheit beweisen zu lassen, könnte schon bald Standard werden.
    On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
    From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
  • In formalen Spezifikationen wird es wirklich wichtig sein, dass Menschen sie interpretieren und verfassen können.
    Meine Sorge ist, dass schwer entzifferbare Mathematik entsteht und eine kleine Glaubensgemeinschaft sie bewacht. Verschiedene obskure Notationen sind nicht kompatibel, und selbst wenn man eine versteht, hilft das beim Verständnis einer anderen womöglich kaum. Die meisten werden am Ende nur englische Sätze schreiben, die sich nicht ordentlich verifizieren lassen.
    Noch schlimmer wäre es, wenn man Maschinen ihre eigenen Aussagen formalisieren lässt, ohne den Formalismus oder den Beweis zu verstehen, und dann an einem Verifikationstheater teilnimmt, um anschließend überrascht zu tun, wenn alles auseinanderfliegt.
  • Mich würde interessieren, ob du dir Ada/SPARK angesehen hast. Falls ja, würde mich auch interessieren, ob es deiner Intuition davon entspricht, wie die Dinge eigentlich laufen sollten.
    Es gibt langsame Fortschritte dabei, solche Fähigkeiten in die Bereiche zu integrieren, die Typsysteme nicht schnell abdecken können, deshalb interessieren mich die Perspektiven von Leuten, die diesen Weg schon früher gegangen sind.

• Gut. In den letzten Monaten habe ich in Scala 3 mit ausdrucksstarken Typen gearbeitet, sodass Typen nach und nach mehr Beweise zur Compile-Zeit tragen. Ich benutze keine Makros, aber ein paar wären wohl nützlich.
  Dieser Ansatz scheint nicht nur dabei zu helfen, das Problem sich ausbreitender agentischer Tests zu reduzieren, sondern auch zu verhindern, dass Agenten in minderwertige Arbeitsweisen abrutschen. Insbesondere verhindert er eine Anhäufung von Substantiven, bei der der Agent für alles neue Singleton-Typen anlegt, selbst wenn er sinnvollerweise generalisieren sollte.
  Ich denke, dass die Beschleunigung hochwertiger agentischer Programmierung eher von Werkzeugen kommen wird, die formalen Methoden ähneln, einschließlich Sprachen mit starken Typsystemen.
  Mit ausdrucksstarken Typen meine ich hier Techniken, die man nicht in eine normale Codebasis einbringen möchte, wenn das Team nicht bereits mit Type-Level-Programmierung vertraut ist. Es muss also ein Team sein, für das Higher-Kinded Types und Typfunktionen keine seltsamen Dinge sind, sondern Grundbausteine.
  Agenten sind in Bezug auf Wissen in den meisten Fällen „mathematischer“ als die meisten Entwickler und oft sogar besser als von Kategorientheorie geprägte Entwickler. Außerdem haben sie für Konversationen gewissermaßen „unendliche“ Geduld, daher eignen sie sich auch ziemlich gut zum Lehren.
  Ich persönlich habe Codex einige Hobby-Beweise in Lean-Stil übertragen lassen, und das war sehr einfach. Ich würde nicht behaupten, dass es zu 100 % „korrekt“ ist, und um das gründlicher zu prüfen, müsste ich Lean 4 besser lernen, aber es scheint zumindest die klassischen Fallen in Beweisen zu überprüfen. Ich freue mich sehr auf die Zukunft formaler Methoden.

• Es wirkt wie die Aussage, dass Gen AI so viel Code erzeugt, dass wir den menschlichen Wert stärker in Richtung Verifikation verlagern sollten. Ich denke gelegentlich darüber nach, was Programmierung eigentlich wirklich ist
  Wenn Englisch nicht die Muttersprache ist, ist schon das Erlernen des Programmierens selbst eine große Herausforderung. Um nicht übersetzte englische Dokumentation zu verstehen, muss man sich auf maschinelle Übersetzung verlassen, und Material in der eigenen Sprache hinkt 5–6 Jahre hinterher
  Jetzt, da es unmöglich wird, Zehntausende von von AI erzeugten Codezeilen per Code Review zu prüfen, sieht man Diskussionen darüber, absolute Regeln wie mathematische Beweise aufzustellen. Beim Lesen dieses Artikels musste ich an den Borrow Checker von Rust denken. Wenn man Rust tatsächlich ein paar Mal benutzt, führt das oft zu der schlechten Gewohnheit, Tricks zu suchen, um den Borrow Checker zu umgehen
  Wenn mathematische Strenge zu weit geht, suchen Menschen nach Umwegen. Programmierer mit wenig Ausbildung wie ich neigen besonders dazu
  Es scheint, als würden solche Versuche am Ende dazu führen, Code nur noch für bestimmte formalisierte Antworten zu schreiben. Wenn das so standardisiert wird, bin ich nicht sicher, ob es noch auf menschliche Anforderungen reagieren kann
  Solche defensiven Programmieransätze finde ich in Ordnung, aber ich möchte das machen, was ich in meinen eigenen Worten aggressive Programmierung nenne. Also Risiken eingehen, schnell beheben und ausliefern und darauf vertrauen, dass es mit der Zeit gut genug wird
  Natürlich passt der Ansatz des Artikels für etablierte Branchen wie Jane Street, wo Genauigkeit wichtig ist und der Arbeitsbereich klar definiert ist. Dort gibt es genug Daten, um die Anforderungen des Marktes angemessen zu modellieren
  Aber für soziale Verlierer wie mich, die ständig weiterziehen, um Goldminen zu finden und Geld zu verdienen, wirkt diese Methodik wie ein Luxus. Ich weiß, dass bestehende Geschäfte mit ausgereiftem Modeling fortlaufend von hochqualifizierten Fachkräften optimiert werden müssen und man mit dieser Nachfrage realistisch nicht Schritt halten kann. Deshalb suche ich nach Bereichen, in denen das Modeling nicht strukturiert ist, aber ich weiß nicht, ob man diesen Ansatz auch dort anwenden kann

  • Man muss es aus der Perspektive von Jane Street betrachten. Sie sind ein High-Frequency-Trading-Unternehmen und handeln Aktien und Finanzprodukte in Hunderttausender-, vielleicht sogar Millionenhöhe
    Dort gibt es kein „man kann es später reparieren“. Wenn man versteht, was schiefgelaufen ist, kann man bereits Milliarden verloren haben
    Deshalb kann ein aggressiver Ansatz in nicht zum Kerngeschäft gehörenden Bereichen funktionieren
    Nebenbei: Defensive Ansätze werden bereits überall eingesetzt. In Python, Java usw. gibt es Garbage Collector, und damit wird gewissermaßen verifiziert, dass der Code wie beabsichtigt ausgeführt wird
    Ich habe mich gefragt, ab wann formale Verifikation sichtbar werden würde, aber vom Stadium, in dem man sich um Implementierungsdetails sorgt, zu dem überzugehen, in dem man Probleme wissenschaftlich und mathematisch beschreibt, ist ein natürlicher Schritt
  • Ich mag die Formulierung „aggressive Programmierung“. Allerdings ist dieses Paradigma bereits der Grundzustand der Branche
    Wegen Gen AI sind die Kosten defensiver Programmierung stark gesunken, während die Kosten menschlicher Verifikation stark gestiegen sind. Formale Methoden machen Verifikation dagegen billig, aber der Implementierungsaufwand ist hoch: Man muss Spezifikationen, Typen und Beweise schreiben und die Implementierung in ein starres Raster biegen
    Doch Gen AI kann genau diese mühsame Arbeit automatisieren. Die beiden passen perfekt zusammen
  • Wenn du dich bei nicht übersetzten englischen Dokumenten auf maschinelle Übersetzung verlässt, dann empfehle ich dir, auch wenn es etwas am Thema vorbeigeht, dringend, Englisch zu lernen
    Das kostet etwas Mühe, aber wenn man den fortlaufenden Übersetzungs-Overhead beseitigt, wird das enorm helfen
  • Ich stimme zu, dass diese Methodik ein Luxus ist. Auch der Artikel erkennt das an, und Jane Street ist eine ziemlich speziell aufgestellte Organisation, die von diesem Ansatz profitiert
  • Natürlich hat Jane Street so einen Text veröffentlicht, weil er für sie relevant ist, und natürlich lässt er sich nicht allgemein auf jede Art von Programmierung anwenden
    Ich verstehe nur nicht ganz, wie es mit diesem Punkt zusammenhängt, sich selbst als „sozialen Verlierer“ zu bezeichnen oder zu sagen, dass man solche Praktiken in der eigenen Karriere nicht verfolgt

• Ich spiele in letzter Zeit mit verwandten Ideen herum, und was mich überrascht hat, war, wie gut Frontier-Modelle, insbesondere ChatGPT-5.5, bestimmte manuelle Beweise in Roqc, dem früheren Coq-Proof-Assistant, vervollständigen können
  Die Beweise sind nicht immer elegant, aber ChatGPT beweist oft in wenigen Minuten und innerhalb von 10–100 Iterationen Dinge, für die ich mit begrenzter, aber nicht null Erfahrung mit Proof Assistants und ziemlich viel Domänenwissen über den Bereich der zu beweisenden Hilfssätze deutlich länger brauchen würde
  Im Kontext dieses kurzen Textes ist das deshalb interessant, weil es eine Grundannahme bestimmter Werkzeuge für formale Methoden erschüttert. Frama-C, Ada/SPARK usw. konzentrieren sich darauf, Proof Obligations zu erzeugen, die von Werkzeugen wie CVC5 oder Z3 automatisch aufgelöst werden können; wenn das scheitert, wechselt man zu der ziemlich schmerzhaften Alternative manueller Beweise in Roqc
  Ein üblicher Ablauf ist, festzustellen, dass eine bestimmte Obligation „schwierig“ ist, also nicht automatisch aufgelöst wird, und dann die Menge an Hilfssätzen und Assertions, die am Entstehungspunkt dieser Obligation im Code sichtbar sind, umzuformen, um sie „leicht“ zu machen, oder sogar den Code selbst zu ändern
  Das ergibt Sinn in einer Welt, in der Roqc-Beweise doppelt so teuer sind. Für Menschen sind sie schwer zu schreiben, und wenn sich Code und umgebende Beweise ändern, ist der Wartungsaufwand ebenfalls sehr schwankend
  Wenn Roqc-Beweise aber zu „automatischer Auflösung mit AI in der Schleife“ werden, verschwindet dieser Kostenunterschied. Dann kann man Beweise wie Code schreiben und menschenlesbare Klarheit zur obersten Priorität machen, während Optimierung für Compiler oder Prover erst viel später kommt. Die Implikationen habe ich noch nicht vollständig verarbeitet, aber ich finde sie ziemlich spannend

  • Wie wahrscheinlich ist es, dass AI in einer Situation, in der sich Anforderungen geändert haben und etwas nicht mehr beweisbar ist, Code und Anforderungen selbst verändert, nur um den Beweis leichter zu machen?
    Ich habe mich nie mit Beweisen beschäftigt, aber ich habe gelegentlich gesehen, dass AI, wenn man sagt „nach der Änderung schlägt dieser Test fehl“, statt den Code so zu korrigieren, dass sowohl der bestehende als auch der neue Test bestehen, einfach den Test selbst verändert
  • Das entspricht auch meiner Erfahrung, aber ich habe mich für Lean entschieden. Das war stärker mit der Funktion verknüpft, die ich bauen wollte
    Ich freue mich auf die Zukunft
  • Wenn du sagst, dass ChatGPT Roqc-Beweise in wenigen Minuten und innerhalb von 10–100 Iterationen schafft, frage ich mich, wie man weiß, ob der Beweis selbst korrekt ist

• Jedes Mal, wenn ich über formale Spezifikationen lese, wirkt es auf mich wie „dieselben Tests auf eine andere Art geschrieben“, oder schlimmer noch wie „dieselbe Implementierung auf eine andere Art geschrieben“
  Es kann zwar helfen, Fehler zu finden, wenn man etwas zweimal schreibt, aber wenn formale Spezifikationen dieselben Bugs haben können wie Tests oder die Implementierung, verstehe ich nicht so recht, was daran besonders ist
  Das grundlegende Problem scheint mir zu sein, dass man, um formal zu beweisen, dass ein Programm irgendetwas tut, dieses „irgendetwas“ sehr konkret definieren muss. Dann schreibt man im Grunde die Tests oder die Implementierung noch einmal
  Ich habe mich über mehrere Jahre immer wieder sporadisch mit dem Thema beschäftigt und habe ständig das Gefühl, dass mir etwas entgeht, aber ich weiß nicht, was. Kann das jemand erklären?

  • Wie Dijkstra bekannt sagte: „Program testing can be used to show the presence of bugs, but never to show their absence“
    Der Mangel von Tests ist, dass man nur Verhalten testen kann, von dem man glaubt, dass es problematisch sein könnte. Um auch Verhalten proaktiv abzusichern, von dem man nicht einmal wusste, dass es schiefgehen kann, braucht man ungewöhnlichere Werkzeuge im Werkzeugkasten. Fuzz-Testing ist ein Anfang in diese Richtung, und formale Verifikation ist ein weiterer
    Natürlich hängt die Qualität solcher Werkzeuge davon ab, wie gut man ein umfassendes formales Modell schreibt, das gewünschtes Verhalten erlaubt und unerwünschtes Verhalten verbietet, und in vielen Bereichen sind wir davon immer noch überraschend weit entfernt
  • Der große Unterschied ist, dass formale Methoden es erlauben, den Allquantor für alles zu verwenden
    In einem Unit-Test kann man zum Beispiel schreiben: „foo('abc') gibt einen String ohne nachgestellte Leerzeichen zurück“
    Mit formalen Methoden kann man aber beweisen: „Für jede beliebige Eingabe x gibt foo(x) einen String ohne nachgestellte Leerzeichen zurück“
    Ein triviales Beispiel, aber man kann sich auch Komplexeres vorstellen wie „Für jedes beliebige Programm P verhält sich compile(P) wie P“
    Natürlich muss man definieren, was „dasselbe Verhalten“ bedeutet
  • Ich arbeite zwar nicht mit Software, aber bei ASIC- und FPGA-Designs ermöglichen formale Methodenspezifikationen, mit Werkzeugen wie SAT-Solvern zu entscheiden, ob ein Zielentwurf die Spezifikation erfüllt
    Man spezifiziert Eigenschaften des Designs, und das Werkzeug testet den Entwurf auf verschiedene Weise, um zu prüfen, ob diese Eigenschaften verletzt werden können
    Bei einem System zur Steuerung von Ampeln könnte man zum Beispiel die Eigenschaft angeben, dass sich kreuzende Fahrspuren nicht gleichzeitig oder nicht innerhalb eines bestimmten Zeitraums beide Grün bekommen dürfen
    Das Werkzeug prüft dies per erschöpfender Suche und kann einen Code-Pfad zeigen, der die Eigenschaft verletzt
  • Es ist mehr als nur „dieselben Tests auf eine andere Art geschrieben“. Einzelne Tests sind meist voneinander unabhängig oder werden unbeherrschbar groß, und die Vollständigkeit einer Testsuite muss man mit relativ groben Überlappungsmaßen wie Branch Coverage beurteilen
    Ein statisch bewiesenes Typsystem sorgt dafür, dass jede Komponente im Voraus gegen alle anderen geprüft wird. Es garantiert nicht einfach nur „dieser Test besteht“, sondern beim Zusammensetzen „all diese Tests bilden ein sinnvolles und konsistentes Ganzes“, und verhindert, dass ein inkonsistentes Modell im Code umgesetzt wird
    Das ist ähnlich wie bei Rusts match, das verlangt, alle möglichen Zweige vollständig abzudecken, nur auf die Größenordnung einer ganzen Codebasis hochskaliert
    Es stimmt, dass damit grundlegende Logik- oder Theoriefehler nicht abgefangen werden. Aber man könnte überrascht sein, wie viel robuster es ist als etwa die Kombination aus Haskells Typsystem, ad-hoc funktionalen Tests und Property-Tests. Auch das ist insgesamt ein starkes System, aber formal bewiesene Kryptographie setzt eine deutlich höhere Messlatte
  • Der starke Unterschied liegt zwischen einem bestimmten Test und einem Vollbeweis. Wenn man einen Grenzfalltest nicht mitdenkt, geht er einfach unter. Mit einem guten Modell kann man seine Existenz schon vor dem Deployment erkennen und beheben
    Besonders wertvoll ist das bei Nebenläufigkeit, verteilten Systemen und Multi-Threading. Race Conditions und Deadlocks sind extrem schwer zu testen und zu durchdenken, ebenso Fragen wie „Können A, B, C in der Reihenfolge A, C, B passieren?“
    Die Reife dieses Bereichs dürfte sich ungefähr so entwickeln: Erstens werden LLMs das Lernen und Anwenden formaler Methoden stark beschleunigen, selbst wenn sie anfangs nur eine nachgelagerte Verifikation nach dem Muster „ein zweites Mal probieren“ liefern
    Zweitens wird es zu Automatisierung übergehen, bei der ein LLM prüft: „Der Implementierungscode hat sich geändert, aber sieht es so aus, als sei das Modell dadurch gebrochen worden?“ Das ist weiterhin nicht deterministisch, aber vermutlich viel besser, als wenn Menschen etwas prüfen müssen, das sich nur gelegentlich ändert
    Drittens wird der eigentliche Sprung darin liegen, Werkzeuge für „Schreibe nur die formale Spezifikation und generiere die Implementierung“ auf die nächste Stufe zu bringen. Es gibt bereits mehrere solche Codegenerierungsprojekte, aber die meisten sind noch nicht vollständig bis zu dem Reifegrad gelangt, den Unternehmen wollen. Was wäre, wenn LLM-Werkzeuge die 1–2 Jahre Handarbeit beschleunigen könnten, die nötig sind, um eines davon an den eigenen Bedarf anzupassen?

• Kleppmanns früherer Artikel https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... ist ebenfalls lesenswert, und natürlich sollte man immer abwägen, was man stattdessen in Typsysteme oder Linter packen kann
  Ich hoffe auf benutzerfreundlichere Ansätze. Von den im Artikel genannten Werkzeugen scheinen dafny und iris der industriellen Nutzung am nächsten zu sein. Soweit ich weiß, hat auch Amazon S3 intern bereits TLA verwendet
  Aber ein TypeScript-Äquivalent für dieses Feld — etwas, das sich natürlich in bestehende Werkzeuge einfügt, wie eine Zero-Cost-Abstraktion funktioniert und das die Leute ehrlich dem bisherigen Ansatz vorziehen — habe ich bisher noch nicht gesehen
  Selbst Custom-Linter zu verwenden ist immer noch ziemlich unerquicklich. golangci-lint ist eine schmerzhafte Codebasis, und semgrep habe ich nicht benutzt, aber seine Rule Engine wirkte einschüchternd. Mit einer AST-API, die mir wirklich gefällt, habe ich auch noch nicht gearbeitet

• Solche Lobeshymnen auf deduktives Schließen, also auf „formale Methoden“, lassen immer ihre grundlegende Grenze aus. Gemeint ist die Frage, wie gut Axiome und Definitionen zur Zieldomäne passen
  Das ist wie der Satz: „Theoretisch gibt es keinen Unterschied zwischen Theorie und Praxis. In der Praxis schon …“ Es wird vermutet, dass Jane Street eine große Codebasis mit einer 1:1-Abbildung pflegt, weil der Zweck des Codes darin besteht, deterministische Algorithmen zu implementieren. Viele Entwickler arbeiten in solchen Bereichen, aber Millionen tun das nicht. Der Großteil der UI und der Großteil explorativer Arbeit gehören dazu
  Parallel zu formalen Methoden gibt es auch eine Strömung, die Akzeptanzkriterien mit hoher Auflösung zu definieren versucht, wenn auch nicht auf logisch-mathematische Weise. Diese Strömung ringt zumindest mit dem Abbildungsproblem, löst es aber an den meisten Orten nicht, an denen die Karte nicht das Territorium ist
  Die Google-Suchergebnisseite verfügt über ein extrem weit entwickeltes internes Optimierungs-Framework, aber hat sie wirklich das Optimum erreicht? Hätte ein schnell gebauter Prototyp, der eine vage Idee einfangen soll, es besser zeigen können? Solche Fragen lassen sich am besten beantworten, wenn man nicht ins Innere des Systems schaut, sondern auf das Außen, dem das System dient

  • Formale Methoden sind genau für Domänen mit wohldefinierter Semantik gedacht
    Logikschaltungen, CPU-Komponenten mit viel formaler Verifikation, Kernel, Protokolle, Parser, Compiler, Kryptografie, Sicherheits-Frameworks, Nebenläufigkeits-Primitiven usw. profitieren stark von Verifikation
  • Die meisten realen UIs laufen letztlich auf Zustandsmaschinen hinaus, und das passt sehr gut zu formaler Verifikation
    Wenn man mehr lernen will, ist der Text von Hillel Wayne ein guter Ausgangspunkt: https://www.hillelwayne.com/formally-specifying-uis/
  • Die Google-Ergebnisseite selbst ist nicht wohldefiniert, aber vermutlich sind über 90 % des darunterliegenden Codes wohldefiniert
    Und in manchen Fällen kann man auch dann lernen, wenn das Ergebnis nicht wohldefiniert ist, also ist es nicht nur ein Problem des Hinsetzens und Nachdenkens darüber, was sinnvoll wäre

• Aus der Sicht von jemandem, der sich ein wenig für Entwurf und Implementierung von Programmiersprachen interessiert, war dieser Satz wirklich faszinierend: „Für die meisten Menschen, die sich mit Programmiersprachen beschäftigen, ist der einfache Teil, neue und bessere Ideen zu haben, die Programmierung verbessern. Der schwierige Teil ist, jemanden davon zu überzeugen, diese Ideen in echter Arbeit einzusetzen“
  Dem stimme ich völlig zu. Selbst wenn es Vorteile gibt, gibt es eine Grenze für die Menge an Fremdheit, die man in eine neue Sprache einbauen kann
  Aber AI-Agenten werden gegenüber radikal neuen Ideen im Programmiersprachen-Design vermutlich keinen großen Widerstand empfinden. Ich denke schon seit einer Weile darüber nach, wie sich Programmiersprachen-Design nach agentischer AI entwickeln wird
  Es wäre sehr spannend zu sehen, welche neuen Ideen man entwickeln könnte, um Programmiersprachen zu verbessern, wenn man sich um Adoption viel weniger sorgen muss
  https://steveklabnik.com/writing/the-language-strangeness-bu...

• Ich arbeite im Bereich Application Security Testing daran, formale Methoden anzuwenden, und denke, dass sich derselbe Ansatz auch auf die Verifikation von Business-Logik anwenden lässt
  Dafür verwenden wir Taint Analysis. Das ist ein recht etablierter Ansatz aus den formalen Methoden, wurde in der Praxis aber wegen der Komplexität des Datenflusses in realen Codebasen bislang noch nicht breit angewendet
  Formale Methoden über AST-Pattern-Matching und einfache Typprüfung hinaus zu erweitern, ist wirklich schwierig. Es hat Jahre an Forschung und Entwicklung gebraucht, bis wir mit Taint Analysis an den Punkt kamen, in echten Codebasen prozedurübergreifende Datenflüsse innerhalb weniger Minuten nachzuverfolgen und tief versteckte Schwachstellen zu finden
  Wer Interesse hat, kann sich das Projekt ansehen: https://github.com/seqra/opentaint

• Vor etwa 18 Monaten habe ich mich darin vertieft, Typen zusammen mit LLMs zu verwenden, und vor etwa 6–8 Monaten wurde es mit lean4 ernst. Inzwischen würde ich nicht einmal mehr erwägen, AI-Unterstützung für Softwarearbeit ohne eine CIC-beweisgestützte Basis mit praktischer C/C++-FFI und damit faktisch Anbindung an alles zu verwenden
  Von JSON bis Python haben wir alles verboten, und auch nix wurde neu geschrieben, damit es einen Compiler gibt. Fast alles, was wir verwenden, wird nicht nur mit Property Testing und mehreren Fuzz-Tests bis ans Limit geprüft, sondern hat mindestens auch einen lean4-Beweis, der über .olean-Linking das Property Testing antreibt. Wenn Zeit da ist, beweisen wir sogar die Vollständigkeit ganzer Domänen und testen diese Eigenschaften ebenfalls
  Alles, was schnell sein muss, wird in lean4 erzeugt, also überspringen wir die C++/Rust-Debatte. Es hat Vorteile, wenn ein C++-Bug in Wirklichkeit ein Bug im lean4-Code ist, aber es kann in beide Richtungen gehen
  Das ist eine große Umstellung, und ich nehme es niemandem übel, wenn er bei „Ihr verbietet JSON und Python?“ skeptisch ist. Aber wir haben auf diese Weise Millionen Zeilen geprüft, und AI + formale Systeme ist ein viel größerer Sprung als der von ohne AI zu AI mit Python. Letzteres verläuft unserer Erfahrung nach nicht monoton, Ersteres dagegen fast immer
  Man kann ziemlich gewagte Dinge tun. Das hier ist ein formaler Beweis für polyedrische Tensorberechnungen, wie sie von Dingen wie ISL und CuTe modelliert werden, und damit kann man auf Geräten mit C++23-mdspan Swizzling und Tiling betreiben und auch noch beweisen, dass es korrekt ist. Dieses Beispiel zeigt allerdings nicht besonders gut ein L'Hopital-artiges Argument zur Coverage: https://github.com/b7r6/mdspan-cute
  Das Ergebnis ist wirklich schnell, und zwar schon beim ersten Versuch
  https://straylight.software/assets/lambda-hierarchy.svg

  • Agda und Idris 2 unter CIC einzuordnen, macht die Lambda-Hierarchie-Grafik selbst bei wohlwollender Betrachtung irreführend
  • Deshalb würde mich interessieren, welche Software damit gebaut wurde und warum sie nützlich ist