Boris Cherny tweetet über TLA+ und das Internet rastet aus
The internet discovers TLA+. Now what?
Ein Tweet von Boris Cherny über TLA+ hat die Aufmerksamkeit auf das 30 Jahre alte formale Modellierungswerkzeug gelenkt. Reasonable erklärt, was TLA+ ist, wo es an Grenzen stößt und wie eine agentische Pipeline 16.000+ TLA+-Spezifikationen in über 3.000 maschinell geprüfte Verus-Beweise übersetzte.
TLA+ beschreibt mögliche Systemverhalten und die Eigenschaften, die diese Verhalten erfüllen sollten.
- lopatin
Ich würde jeden ermutigen, das mal an irgendeinem in sich geschlossenen, zustandsautomatenähnlichen Problem auszuprobieren, falls man sowas hat. Bei meiner Firma haben einige Experten unsere Clustering- und Failover-Logik optimiert, indem sie ein bisschen mehr Zustand (und damit Komplexität) hinzugefügt haben. Obwohl ich in dem Bereich kein Experte bin, konnte ich einen katastrophalen Bug finden und verhindern, indem ich Opus, bewaffnet mit TLA+, auf das Problem angesetzt habe. Es war ein Bug, der in der vorherigen Implementierung des Systems nicht möglich war, und niemand kam auf die Idee, Unit-Tests für die Abfolge von Schritten zu schreiben, die ihn auslöst, also blieb er zunächst unbemerkt. Das Einzige, was ihn aufdeckte, waren die TLA+-Invarianten, die – ja – ebenfalls von Opus geschrieben wurden.
Als Randnotiz: Es wird viel darüber geredet, dass Programmieren keinen Spaß mehr macht. Aber die obige Übung war wahrscheinlich das, was mir am meisten Spaß am Engineering seit Langem gemacht hat, und wäre für mich persönlich ohne KI nahezu unmöglich gewesen. Vielleicht lag es an der Neuheit des TLA+-Krams, aber ich denke, es gibt einen Ausblick darauf, wie unsere Jobs in Zukunft tatsächlich aussehen könnten – jenseits davon, Claude einfach zu sagen, das zu tun, was man früher manuell gemacht hat, und dann Enter zu drücken. Es gibt viel ehrgeizigere und erfüllendere Anwendungsfälle dafür.
- stevefan1999
Ich nutze TLA+ indirekt über https://github.com/quint-co/quint. Ich habe Anweisungen hinzugefügt: „Bevor du irgendein Feature implementierst, modelliere es bitte mit Quint und stelle sicher, dass es kein Gegenbeispiel für das Gesamtsystem gibt; überdenke das Design ebenfalls mit Quint und stelle sicher, dass deine Dokumente und deine Implementierung dem formalen Modell und den Dokumenten folgen.“
Das Ergebnis dauert zwar viel länger, ist aber ziemlich magisch. Viele Transaktions- und Atomizitäts-Bugs wurden allein durch diese einfache Anweisung gefunden und behoben.
Manchmal ist es jedoch nicht ganz so magisch, besonders bei externen Ressourcen. Cloudflare hat leider manchmal Aussetzer bei D1 und KV mit Timeouts, was mehr oder weniger höhere Gewalt ist.
Glücklicherweise bedeutet das, dass ich die Aktion als binäres Ereignis modellieren muss – dass die Transaktion möglicherweise nicht so abgeschlossen wird, wie wir es als garantiert angenommen hätten – und zusätzliche Guards darum herum einbauen muss, sodass der Zustand erneut versucht werden muss.
So konnte ich es bisher umgehen. Denk daran: Je mehr Bedingungen und Einschränkungen, desto stärker muss deine CPU sein, da es in der Größenordnung von NP liegt.
- peterus
Reale Anwendungen von TLA+: https://foundation.tlapl.us/industry/index.html.
Das Intel-Paper zeigt, wie TLA+ als Schritt vor dem Schreiben der Hardwarebeschreibung eingesetzt wurde. Ich bin nicht sicher, ob sich das durchgesetzt hat; es scheint, dass heutzutage andere Tools verwendet werden. Weiß jemand hier aus der VLSI-Branche mehr?
- pron
Ich liebe TLA+, um Systeme präzise und doch knapp zu beschreiben und über sie zu raisonnieren. Aber als jemand, der seit vielen Jahren formale Methoden zur Unterstützung der Softwareentwicklung einsetzt, verwirrt mich diese ganze Industrie um Tools, die eine so wunderbare mathematische Sprache – und andere wie Lean – mit KI verbinden, bis hin dazu, die Argumentation vor den Menschen zu verbergen.
Programme end-to-end als korrekt zu beweisen (d. h. vom Code bis zu High-Level-Eigenschaften) – wie diese Firma und andere es vorgeben zu tun – ist so schwierig, dass Menschen es nur für sehr kleine Programme (~10 KLOC) geschafft haben, und selbst dann in sehr speziellen Fällen, in denen die Programme auf extra einfache Weise geschrieben wurden (oft auf Kosten der Performance, weil Performance häufig kompliziertere Algorithmen erfordert). Wenn KI mindestens eine Größenordnung leistungsfähiger als Menschen in der Softwareentwicklung wird – was für diese Aufgabe nötig wäre –, bräuchte sie dann unsere Hilfe, um verschiedene Tools und Testumgebungen zu schreiben, die bei der Aufgabe helfen? Schließlich ist das Schreiben dieser Tools so viel einfacher als ihre Verwendung für dieses Ziel, dass ich die Hypothese hinter der KI-Fähigkeit hier nicht verstehe.
Diese Firma sagt: Sie „entwickeln die agentischen Frameworks, um diese Korrektheitsgarantien für alle Softwareentwickler zugänglich zu machen“. Aber das alles zu entwickeln ist der leichte Teil! Wenn KI den schwierigen Teil erledigen kann, warum braucht sie dann unsere Hilfe, um das zugänglich zu machen? Sie kann sicher selbst einen Weg finden, diesen leichten Teil zu erledigen! Das ist, als würde man sagen: „Bald haben wir eine Maschine, di […]“
- bsenftner
Hat 10 Minuten gedauert, das zu finden: TLA+ ist eine formale Spezifikationssprache, die entwickelt wurde, um reaktive Systeme zu entwerfen, zu modellieren, zu dokumentieren und zu verifizieren.