● Position · Loop Engineering

„My job is to write loops." — eine Schraube weiter

Wir haben immer auf Blackboxes gebaut und an Schnittstellen validiert. Das Neue ist das Probabilistische. Die Antwort ist, den Determinismus in die Gates zu verschieben.

Cong Chanh Vinzenz Nguyen · F#/.NET

„My job is to write loops." Boris Cherny, der Kopf hinter Claude Code, beschreibt damit die nächste Abstraktionsstufe der Softwareentwicklung: Er promptet den Agenten nicht mehr – er baut die Schleife, die den Agenten anstößt und re-promptet, bis ein verifizierbares Ziel erreicht ist. „Loop Engineering" heißt das.

Die Motivation teile ich – Teile davon praktiziere ich auch: bei Code-Reviews lasse ich via tmux verschiedene Agenten weitgehend autonom prüfen und fixen. Drei Vorbehalte hatte ich aber: lückenlose Spezifikation als Bedingung (sonst iteriert der Loop hartnäckig am Falschen), Cognitive Debt als Preis, und die Tokens, die ein Brute-Force-Loop verbrennt. Ich möchte einen Gedanken nachschieben, der die drei zusammenhält – und ehrlich gefragt: Kommt das so hin?

Wir bauen seit jeher auf Blackboxes

Der interessanteste Teil hängt für mich am Blackbox-Motiv. Denn ehrlich gesehen bauen wir seit jeher auf Blackboxes. Kaum jemand versteht die ganze Kette vom Transistor über ISA, Compiler und Betriebssystem bis zum gerenderten GUI. Wir beherrschen das nicht durch Vollverständnis, sondern an den Schnittstellen: Typen, Tests, Design by Contract. Und selbst die deterministischen Schichten vertrauen wir nicht blind – wir validieren sie. Der Compiler gilt nicht als korrekt, weil er deterministisch ist, sondern weil Jahrzehnte Praxis und Testsuiten ihn gehärtet haben; bei CompCert sogar ein formaler Coq-Beweis. Das ORM ist der Paradefall der leckenden Abstraktion (Spolsky): N+1, Transaktionsisolation, Lazy Loading bluten durch. Determinismus macht einen Fehler reproduzierbar, nicht abwesend. „Validieren statt blind vertrauen" galt also schon vor den LLMs – Cognitive Debt auch.

Wo die Analogie bricht: probabilistisch statt deterministisch

Und hier bricht die Analogie – genau der Bruch ist die Pointe: Die KI reiht sich nicht nahtlos in diesen Stack ein. Compiler und ORM sind im Kern deterministische Abbildungen ihres Inputs (modulo der bekannten Reproducible-Builds-Themen). Ein LLM ist intrinsisch probabilistisch – es modelliert eine Verteilung über Tokens, keine Funktion; selbst bei Temperatur 0 nicht garantiert bit-identisch (Floating-Point-Nichtassoziativität auf GPUs, variables Batching). Die saubere Achse ist also nicht „deterministisch vs. probabilistisch" allein, sondern: spezifizierter, getesteter Kontrakt vs. statistischer Generalisierer ohne Korrektheitsgarantie. Drei Annahmen, auf denen klassische Abstraktion ruht, fallen damit weg: Determinismus, spezifizierte Schnittstellen-Semantik, einmal amortisierte Verifikation. Die untere Schicht validiere ich einmal und vertraue ihr dann millionenfach. KI-Output muss ich pro Aufruf neu validieren.

Der Vorschlag: den Determinismus in die Gates verschieben

Daraus mein eigentlicher Vorschlag – Loop Engineering eine Schraube weiter: die Gates härten. Nicht den Agenten deterministisch machen, das geht nicht. Sondern die Akzeptanz-Entscheidung. Für die Klasse von Kriterien, die sich als entscheidbare maschinelle Checks ausdrücken lassen – universell quantifizierte Verträge (Design by Contract), Property-Based Tests, Typen, bounded Verifikation –, wird aus „Agent sagt fertig" ein reproduzierbares Pass/Fail. Der Generator bleibt probabilistisch; nur das Urteil über ein gegebenes Artefakt wird stabil. Das eliminiert die Stochastik nicht, es hegt sie ein: Nur was die Gates passiert, gilt als fertig.

Und das prüfende Orakel muss vom Generator getrennt sein – schreibt dasselbe Modell Spec und Code, benotet sich der Agent selbst (korreliertes Versagen). Genau diesen Common-Mode-Defekt hat VeriAct gemessen (arXiv:2604.00280): Die Trennung trägt nur, wenn die Spec aus unabhängiger Quelle kommt – der Mensch ist hier der Dekorrelator, nicht der Loop.

Drei ehrliche Grenzen

Erstens das alte Test-Orakel-Problem: Das Gate prüft die formalisierten Kriterien, nicht den wahren Intent. Ein Gate kann falsifizieren, nie vollständig verifizieren („Tests zeigen Anwesenheit, nicht Abwesenheit von Fehlern", Dijkstra), und nach Rice ist keine nicht-triviale semantische Eigenschaft allgemein entscheidbar. Das ist kein Defekt, das ist die Reichweite. Das Restrisiko verschwindet nicht – es wandert in die Vollständigkeit der Spec; und für UX, „fühlt sich richtig an", emergente Architektur gibt es kein mechanisches Orakel. Genau das sind die Findings, für die der Loop mich doch wieder braucht.

Zweitens terminiert ein Loop über einem deterministischen Akzeptanz-Prädikat nicht von selbst. Das Gate bestimmt, WAS akzeptiert wird – nicht OB und WIE SCHNELL der Loop ankommt. Es braucht ein hartes Iterations- und Token-Limit, das „gib auf, frag den Menschen" sagt.

Drittens die Cognitive Debt. Und hier liegt der eigentliche Punkt nicht an der Blackbox – die ist, wie gesagt, der Zweck von Abstraktion, kein Mangel. Die Grenze ist die Rekonstruierbarkeit des mentalen Modells. Klassisch geschriebener Code hatte einen Autor, der den Intent gehalten hat; das „Warum" ist – wenn auch nicht für jeden unmittelbar – im Code hinterlegt und lässt sich wiedergewinnen. Bei einem Loop, der sich per Brute Force an ein bestandenes Testergebnis herantastet, kann es dagegen sein, dass dieses „Warum" zu keinem Zeitpunkt in einem Kopf existiert hat. Cognitive Debt heißt dann nicht „gerade kennt niemand das Modul", sondern „das Modell ist nicht mehr herleitbar". Genau hier setzt der Vorschlag ein zweites Mal an: Eine formale, maschinenprüfbare Spec ist nicht nur ein Filter, sondern lesbares, geteiltes Systemwissen – der Versuch, das „Warum" herleitbar zu halten, nicht in einem Kopf, sondern als versioniertes, prüfbares Artefakt. Storey nennt dessen Fehlen Intent Debt (arXiv:2603.22106). Ehrlich bleibt die Spannung: Die Spec macht den Intent sichtbar und prüfbar, sie tilgt ihn nicht automatisch (sie kann selbst falsch sein), und sie deckt nur den formalisierbaren Teil des „Warum" – UX, Geschmack, Architektur-Rationale bleiben menschlich gehalten.

Zu den Tokens

Tendenziell sollten präzise Gates sparen, weil falsche Pfade früher abbrechen und gerichtetes Signal statt blindem Retry kommt. Aber das ist ein Trade-off, kein Gesetz: Die Spec selbst kostet Tokens und Menschenzeit, und ein zu hartes oder schlecht getroffenes Gate kann mehr Reparatur-Runden erzwingen statt weniger. Netto bleibt das eine empirische, projektabhängige Frage. Bei mir hat in zwei kleinen Fällen eine einzige Invariant-Zeile einen unbeschränkten Eingaberaum abgedeckt, den eine Beispieltabelle nur zeilenweise erwischt. Das ist ein Existenznachweis, keine Statistik – und nicht jeder hat ein AI-Lab im Rücken.

Womit man die Gates baut: F#, FsCheck, Lean

Ich nenne, wozu ich selbst greife – mit den Kosten zuerst, sonst betreibe ich genau das Marketing, von dem ich mich abgrenze. Kein Geheimtipp, kein Allheilmittel, sondern eine begründete Empfehlung für die Fälle, in denen sich das tragende Kriterium überhaupt formalisieren lässt.

F# kostet: kleinere Community, weniger Stellen, ein Umdenken weg vom imperativen Reflex – von „wie mache ich das" zu „welche Zustände sind überhaupt legal". Was es dafür kauft: Discriminated Unions machen die im Typ modellierten illegalen Zustände unrepräsentierbar – ein billiger Prüf-Schritt, den der Compiler bei jedem Build nachrechnet und der eine ganze Klasse von Agenten-Fehlern gar nicht erst entstehen lässt (nur diese Klasse – Logikfehler in erlaubten Zuständen bleiben). FsCheck (Property-Based Testing) ist dann das praktische Gate über unbeschränkten Eingaberäumen statt einer handgepflegten Beispieltabelle: eine Property als Stichprobe über den ganzen Raum, nicht eine Zeile pro Beispiel. Und es ist kein Spielzeug: volles .NET-Ökosystem, ein C#-Team kann inkrementell adoptieren, erst die Kern-Logik, dann mehr.

Lean 4 kostet mehr: eine steile Lernkurve, Produktionsadoption ist real winzig, und Modell-Treue ist Handarbeit – das Bewiesene muss dem laufenden Code wirklich entsprechen, sonst beweist man ein Phantom. Es lohnt nur für die wenigen Invarianten, die tragend sind (Werterhaltung, Sicherheit), nicht für alles. Dafür liefert es das stärkste Gate, das ich kenne: einen Beweis über alle Fälle statt einer Stichprobe, und sorry-frei heißt buchstäblich keine Lücke – genau die Garantie-Klasse, die ein Property-Test prinzipiell nicht geben kann. Konkret: Ich habe es in einem kleinen Projekt für eine tragende Invariante (Werterhaltung) bis zum sorry-freien Beweis durchgezogen; alle weiteren Invarianten bleiben FsCheck-Property bzw. Roadmap. Genau dieser Aufwand ist auch der Grund, warum es sich nur für wenige Invarianten lohnt.

Der gemeinsame Nenner ist die formale Spec selbst – und damit die Brücke zurück zu oben. Sie ist die deterministische Prüfschicht, die den probabilistischen Generator einhegt, und zugleich der externalisierte Intent. Das ist nicht meine Idee: Lahiri (Microsoft Research) nennt „Intent Formalization" eine Grand Challenge für zuverlässiges Coding mit KI-Agenten (arXiv:2603.17150), und Storeys Intent Debt prägt den Begriff. Mein Beitrag ist nicht die These, sondern eine getypte, lauffähige Implementierung davon. Diese Werkzeuge sind in der Mainstream-Industrie unterrepräsentiert – nicht weil sie schlechter wären, sondern weil der Engpass bisher das Tippen war; jetzt verschiebt er sich zur Prüf-Stärke, und da spielen sie ihre Stärke aus.

Was bleibt

Eine Grenze bleibt auch hier: verifizierer-akzeptiert ist nicht dasselbe wie korrekt, eine Spec kann selbst falsch sein, und nicht jede Domäne hat ein sauberes Modell. Das tragende Kriterium muss gesetzt werden – diese Setzung liegt außerhalb des Entscheidungsproblems (ein zweiter Agent könnte sie ebenso treffen); der Mensch trägt sie, weil er rechenschaftspflichtig ist, nicht weil sie sich grundsätzlich nicht mechanisieren ließe. Wo es ein sauberes Modell gibt, ist es der Unterschied zwischen „der Agent sagt fertig" und „die Eigenschaft hält, geprüft".

Wie Cherny seine Loops konkret betreibt und was er damit tatsächlich baut, dazu findet man erstaunlich wenig. Und bei Sätzen wie „Coding is solved" frage ich mich immer, wo Marketing endet und Realität beginnt.

Kommt das so hin? Wer verschiebt den Determinismus schon bewusst in die Gates – harte, maschinell prüfbare Akzeptanzkriterien statt „Agent sagt fertig", mit getrenntem Prüf-Orakel? Und wo stoßt ihr auf das Oracle-Problem – Ziele, für die es kein mechanisches „fertig" gibt?
→ Das Terminierungs-Orakel: Code, Paper, Belege Die Idee in 5 Min

Quellen