Der Artikel kritisiert die Programmiersprache Bend 2 als exemplarisches Beispiel für die sogenannte „Vibe-Coding“-Falle, bei der Entwickler durch den unkritischen Einsatz von LLMs Systeme von Grund auf neu erfinden, ohne existierende Fachgebiete wie die formale Verifikation zu recherchieren. Anhand des Spiel-Demos von Bend 2 wird aufgezeigt, dass das System extrem umfangreiche Spezifikationen (58 Zeilen) und manuelle Beweise (442 Zeilen) erfordert, während etablierte Alternativen wie SPARK dieselben Bedingungen mit einem Bruchteil des Codes und automatischen Prüfungen durch GNATprove (12 Checks) lösen. Dies verdeutlicht, dass ungezieltes Vibe-Coding oft zu redundanten, ineffizienten und technologisch veralteten Software-Architekturen führt.
Wichtigste Punkte
Bend-2-Demo-Komplexität: Bend 2 erfordert für das offizielle Demo-Beispiel 58 Zeilen Gesetz-Definitionen (LAWS.bend) und 442 Zeilen manuelle LLM-generierte Beweise (PROOF.bend).
Fehlende Literaturrecherche: Vibe-Coding verleitet Entwickler dazu, funktionierende Lösungen zu generieren, ohne das jahrzehntelange Fachwissen und die Werkzeuge des bestehenden Feldes der formalen Verifikation einzubeziehen.
SPARK-Vergleich: Dasselbe Programmlogik-Problem lässt sich in der formal verifizierbaren Programmiersprache SPARK kompakt und komplett abbilden.
Automatisierte Verifikation: Das SPARK-Beispiel wird über den Compiler-Befehl GNATprove vollständig und ohne manuelle Beweisschritte in genau 12 automatischen Checks verifiziert.
LLM-Ineffizienz: LLMs generieren standardmäßig langwierige First-Principles-Lösungen, anstatt effizient auf existierende Industriestandards, Bibliotheken oder automatisierte SMT-Solver hinzuweisen.
Diskussions-Highlights
Kritik an der Autoren-Prämisse: Mehrere Kommentatoren wiesen darauf hin, dass der Autor von Bend 2 (bekannt aus dem Projekt Formality und früheren Arbeiten an dependently-typed Sprachen) sehr wohl über formale Methoden Bescheid weiß, was die ursprüngliche Behauptung des Artikels (Unkenntnis des Feldes) entkräftete und zu einer nachträglichen Notiz des Autors führte.
Usability formaler Methoden: Es wurde diskutiert, dass traditionelle formale Werkzeuge (wie Coq oder Haskell-Derivate) für den Masseneinsatz zu kompliziert sind (z. B. manuelle Definition von Peano-Zahlen), weshalb ein echter Bedarf an einfacheren Syntaxen wie Design by Contract in Standardsprachen (C#, JavaScript) besteht.
Incentives von LLM-Anbietern: Kommentatoren kritisierten, dass kommerzielle LLM-Plattformen (OpenAI, Anthropic, Google) auf schnelle Interaktionen optimiert sind und Anfragen nach umfassender Vorab-Recherche (Prior-Work-Research) erschweren, da das Neuerfinden von Code mehr Tokens verbraucht und den wirtschaftlichen Interessen der Anbieter dient.
Technische Alternativen: Diskutiert wurden die unterschiedlichen Kompromisse zwischen automatischen SPARK-/SMT-Ansätzen und ausdrucksstärkeren, aber aufwendigeren dependently-typed Systemen (wie QTT / Quantitative Type Theory oder Lean), die für allgemeine mathematische Formalisierungen flexibler sind.
Glossar
Vibe-Coding: Ein Begriff für die Softwareentwicklung, bei der Entwickler primär hochrangige Prompts an LLMs übergeben und den Code automatisch generieren lassen, ohne die Implementierungsdetails manuell zu schreiben oder tief zu verstehen.
Formale Verifikation: Der mathematische Nachweis, dass ein Programm oder ein Algorithmus eine bestimmte formale Spezifikation oder ein definiertes Korrektheitsverhalten exakt einhält.
SPARK: Eine hochverifizierbare Teilmenge und ein Werkzeugset der Programmiersprache Ada, die speziell für die Entwicklung kritischer, fehlerfreier Software („mission-critical software“) entwickelt wurde.
GNATprove: Das offizielle statische Analyse- und Verifikationswerkzeug der SPARK-Umgebung, das automatisiert Beweisverpflichtungen (Proof Obligations) prüft.
SMT-Solver (Satisfiability Modulo Theories): Automatisierte Software-Werkzeuge, die prüfen können, ob mathematische Formeln innerhalb bestimmter logischer Theorien erfüllbar sind, und zur automatischen Programmanalyse genutzt werden.
Dependently-typed Language (Abhängig getypte Sprache): Eine Programmiersprache, deren Typsystem Ausdrücke und Werte direkt als Typen einbetten kann, wodurch komplexe mathematische Eigenschaften und Beweise direkt im Code-Typsystem erzwungen werden.
QTT (Quantitative Type Theory): Ein formelles Typsystem, das die Häufigkeit der Verwendung von Variablen im Programmcode streng kontrolliert und häufig in modernen funktionalen Sprachen für Beweiszwecke eingesetzt wird.
Coq / Lean: Interaktive Theorembeweiser (Proof Assistants), mit denen mathematische Theoreme und Programmkorrektheiten maschinell und formal bewiesen werden.