Ideen & Einblicke

AI-First-Entwicklung, Coding-Leitplanken und die Architektur der Entsorgbarkeit erkunden.

model-checkingllmrustformal-proofs

LLMs können Rust-Code generieren. Formale Beweise sind ein ganz anderes Problem.

Große Sprachmodelle schreiben erstaunlich guten Rust-Code, aber wenn man sie um einen formalen Beweis bittet, halluzinieren sie Invarianten und erfinden Syntax, die kein Verifizierer akzeptiert. Hier ist, was sie tatsächlich richtig machen, wo sie scheitern und wie man sie dennoch nutzen kann.

LLMs können Rust schreiben, das kompiliert und sogar besteht. Was sie nicht zuverlässig können, ist einen formalen Beweis dafür zu führen, dass der Code für…
model-checkingtemporal-logicformal-methodsverification

Sie können Code mit einem Model Checker verifizieren, ohne Temporal Logic zu lernen

Bounded Model Checker wie Kani und relationale Model Finder wie Alloy ermöglichen die Verifikation von Eigenschaften mit gewöhnlichen Assertions und Constraints. Sie geben Liveness-Beweise auf, dafür ist die Lernkurve auf Stunden statt Wochen gemessen.

Sie müssen keine lineare temporale Logik lernen, um einen Model Checker zu verwenden. Tools wie Kani, CBMC und Alloy ermöglichen die Verifikation von…
model-checkingrustverificationformal-methods

Man kann Rust-Code korrekt beweisen, ohne einen einzigen Beweis zu schreiben – aber der Zustandsraum ist die Rechnung

Model-Checking-Tools wie Kani erlauben es, Rust-Eigenschaften mit Assertions statt formaler Beweise zu verifizieren. Das Problem ist, was passiert, wenn deine Schleifen keine kleinen Grenzen haben.

Man kann Rust-Code korrekt beweisen, ohne einen einzigen Beweis zu schreiben. Das Tool, das das macht, heißt Model Checker, und für Rust ist der praktischste…
dsls-bounded-contextllmconstrained-generationgrammar

Grammar-constrained decoding: Wie man LLMs zwingt, bei jedem Token valide Syntax auszugeben

LLMs halluzinieren Syntax, weil sie Tokens probabilistisch sampeln. Grammar-constrained decoding filtert das Vokabular in jedem Schritt, sodass nur Tokens emittiert werden, die die syntaktische Gültigkeit erhalten.

Bitten Sie einen LLM, ein JSON-Objekt zu generieren, und er wird irgendwann ein abschließendes Komma ausgeben, einen nicht escapten Zeilenumbruch innerhalb…
dsls-bounded-contextdesign-systemsllmthemes

Vom Englischen ins Theme zu übersetzen ist einfach. Es deterministisch zu machen, ist das eigentliche Problem.

Du kannst Design-Tokens aus einfachen englischen Beschreibungen generieren, aber nur, wenn du die Beschreibung als DSL mit begrenztem Kontext, Schema-Vertrag und Snapshot-Tests behandelst.

Ja, du kannst ein Theme auf Englisch beschreiben und ein funktionierendes Design-System erhalten. Der Haken ist, dass die englische Beschreibung kein Prompt…
dsls-bounded-contextdslparser-combinatorstypescript

Weg mit der Grammatikdatei: Schreib deinen DSL-Parser in plain TypeScript

Parser-Generatoren sind für die meisten Bounded-Context-DSLs overkill. Parser-Kombinatoren erlauben es dir, einen funktionierenden Parser in derselben Sprache wie deine Anwendung zu bauen – ohne generierten Code und ohne Build-Schritte.

Wenn du jemals eine Yacc-Grammatikdatei geöffnet und dich gefragt hast, warum das Bauen einer Sprache das Erlernen einer zweiten Sprache erfordert, bist du…