Du arbeitest an einem Softwareprojekt, das über Jahre gewachsen ist. Irgendwann liest du einen Kommentar im Code, der verspricht, dass eine bestimmte Variable nie null sein darf – aber du traust dem Kommentar nicht mehr. Du hast schon zu oft erlebt, dass solche stillen Versprechen durch Refactoring gebrochen wurden, ohne dass es jemand bemerkt hat. Am Ende stehst du vor undefiniertem Verhalten, das sich schwer reproduzieren lässt.
In einer idealen Welt stünden solche Invarianten nicht in Kommentaren, sondern im Typsystem der Programmiersprache. Genau das ermöglichen abhängig typisierte Sprachen wie Lean oder Rocq (früher Coq). Du kannst Bedingungen wie „dieses Array ist mindestens n Bytes lang“ oder „diese Zahl ist eine Primzahl“ formal spezifizieren. Der Compiler prüft automatisch, ob dein Code diese Bedingungen einhält. Das klingt nützlich, hat aber einen hohen Preis: den manuellen Beweisaufwand.
Der Autor des zugrundeliegenden Textes kennt diese Problematik aus eigener Erfahrung. Er beschreibt, wie er ganze Tage damit verbringen kann, relativ einfache Eigenschaften zu beweisen. Das Beweisen selbst macht Spaß, ist interaktiv und herausfordernd, aber es kostet enorm viel Zeit. Besonders frustrierend ist es, wenn man nach stundenlanger Arbeit feststellt, dass die zu beweisende Aussage schlichtweg falsch ist. Diese Erfahrung teilt er mit vielen anderen in der Welt der abhängigen Typen.
Ein bekanntes Beispiel ist das seL4-Projekt, ein formal verifizierter Mikrokernel. Die Entwickler berichteten, dass sie etwa zehnmal so viel Zeit für das Schreiben von Beweisen aufgewendet haben wie für das eigentliche Design und die Implementierung. Am Ende hatten sie mehr als zwanzigmal so viele Zeilen Beweiscode wie C-Code. Diese Kosten haben abhängig typisierte Sprachen zu einer extremen Nische gemacht. Nun bahnt sich eine Veränderung an, und sie kommt von einer unerwarteten Seite: Large Language Models (LLMs).
Stell dir vor, du baust ein komplexes Uhrwerk. Bisher musstest du jedes Zahnrad einzeln mit der Hand feilen und prüfen, ob es perfekt in das nächste greift. Das ist mühsam und fehleranfällig. Jetzt kommt ein automatischer Assistent, der die Passgenauigkeit für dich überprüft – so schnell, dass du kaum noch selbst Hand anlegen musst. Genau das versprechen LLMs in Kombination mit einem Konzept namens Beweisirrelevanz. Bei vielen Beweisen kommt es nur darauf an, dass ein Beweis existiert, nicht wie er im Detail aussieht. Ein LLM kann solche Beweise oft automatisch generieren, ohne dass du dich um die Struktur kümmern musst.
Der Autor hat das getestet und einen Zstandard-Dekompression in Lean geschrieben. Zstandard ist ein modernes Kompressionsverfahren, das gzip als Standard ablöst. Es basiert auf der LZ77-Struktur, nutzt aber eine ausgefeiltere Entropiecodierung namens FSE (Finite State Entropy). Der Autor erklärt, wie FSE funktioniert: eine Zustandsmaschine mit mehr Zuständen als Symbolen. Häufige Symbole bekommen mehrere Zustände zugewiesen, sodass sie im Durchschnitt weniger Bits benötigen. Die Feinheit liegt darin, dass der Encoder nicht nur ein Symbol auswählt, sondern auch entscheiden kann, in welchem Zustand er landet – diese Wahl trägt Information in die Zukunft. Dadurch können echte Bruchteile von Bits codiert werden, was Huffman-Codierung nicht kann.
Die eigentliche Pointe: Der Autor implementierte diesen komplexen Algorithmus in Lean, ohne sich durch einen Berg manueller Beweise kämpfen zu müssen. Stattdessen ließ er die Beweise weitgehend von einem LLM generieren. Das funktionierte erstaunlich gut. Man muss noch aufpassen, dass der Typchecker nicht überlastet wird, aber die Automatisierung reduziert den Aufwand drastisch. Abhängige Typen mit KI-Unterstützung werden deutlich praktikabler.
Für Entwickler, die hohe Zuverlässigkeit brauchen – in der Luftfahrt, Medizintechnik oder bei Kryptobibliotheken – könnten abhängig typisierte Sprachen bald eine echte Alternative sein. Statt wochenlanger manueller Verifikation könnte KI-gestützte Beweisautomation zum Einsatz kommen. Die Technologie steht noch am Anfang, aber die Richtung ist klar: Die Hürden, die abhängige Typen bisher umgeben haben, sinken.
Du musst nicht sofort in Lean einsteigen. Aber du solltest beobachten, wie sich diese Werkzeuge entwickeln. Wenn LLMs zuverlässig Beweise generieren können, wandern formale Methoden aus der Nische in den Mainstream. Dann wirst du dich vielleicht wundern, warum du je darauf vertraut hast, dass ein Kommentar im Code die Wahrheit sagt.
Quelle: imperialviolet.org
