Eine bekannte Quant-Firma vollzieht eine Kehrtwende: Jane Street baut ein Team für formale Methoden auf. Ausgelöst hat den Sinneswandel ausgerechnet das Programmieren mit KI-Agenten.
drweb.de als bevorzugte Quelle auf Google hinzufügenQualitätsgeprüfte Inhalte direkt in Google News & DiscoverJetzt hinzufügen
Lange galten formale Methoden bei Jane Street als zu teuer für den Alltag. In einem Blogbeitrag erklärt Yaron Minsky, der OCaml bei Jane Street einführte, warum sich diese Rechnung gerade verschiebt.
Das Wichtigste in Kürze
- Jane Street hielt formale Methoden 25 Jahre für zu teuer und stellt jetzt ein eigenes Team dafür auf.
- Der verifizierte Mikrokernel seL4 kostete rund 25 Personenjahre für 8.700 Zeilen C-Code.
- Agentisches Coding senkt die Kosten der Beweisführung und erhöht zugleich ihren Nutzen.
- Typsysteme gelten der Firma als leichtgewichtige Vorstufe formaler Methoden.
Was hat sich geändert?
Den Ausschlag gibt agentisches Coding. KI-Modelle übernehmen einen Großteil der mühsamen Beweisarbeit und öffnen die Werkzeuge für mehr Entwickler. Damit kippt die alte Kosten-Nutzen-Rechnung, die formale Methoden jahrelang als Luxus erscheinen ließ.
Wie hoch der Aufwand früher war, zeigt das Beispiel seL4. Der formal verifizierte Mikrokernel verschlang rund 25 Personenjahre, jede Zeile C verlangte etwa 23 Zeilen Beweis. Für sicherheitskritische Kerne lohnt das, für gewöhnliche Software bislang nicht.
Warum gerade jetzt?
Der zweite Grund ist der Prüf-Engpass. KI-Code neigt zu Slop: unnötig komplex, voller Sonderfälle, oft an den Regeln der Codebasis vorbei. Menschen verbringen viel Zeit damit, diesen Code abzunehmen, und genau hier sollen Beweise entlasten.
Hinzu kommt, dass Agenten von Rückmeldung leben. Ein Typsystem, das Wettlaufsituationen ausschließt, beseitigt sie vollständig, nicht nur stichprobenartig wie ein Test. Dieselbe Allaussage liefern stärkere Beweistechniken, was Jane Street auf spürbaren Mehrwert hoffen lässt.
Tests zeigen, dass ein Fall funktioniert, ein Beweis zeigt, dass alle funktionieren. Sobald Maschinen den Code schreiben, wird dieser Unterschied zum entscheidenden Qualitätsmerkmal.
— Michael Dobler, Herausgeber Dr. Web
Was Entwickler daraus lernen
Die Lehre gilt über Jane Street hinaus: Beim Einsatz von KI-Code braucht es härtere Leitplanken. Typsysteme und formale Beweise fangen ab, was eine reine Sichtprüfung übersieht. Property-based Tests ergänzen das.
Für den praktischen Einstieg lohnt der Blick auf die Modelle selbst. Was große Sprachmodelle heute leisten und wo Menschen führen müssen, ordnet unser Ratgeber zu großen Sprachmodellen ein. Dass KI-Oberflächen ohne Gegenmittel gleich aussehen, zeigt unser Beitrag zu Impeccable gegen KI-Slop.
Den vollständigen Gedankengang samt Beispielen hat Yaron Minsky im Jane-Street-Blog veröffentlicht. Prüfen Sie für eigene Projekte, an welchen Stellen Beweise oder strenge Typen den größten Hebel bieten.
Mehr Newshunger?
