.png&w=64&h=64)
Software Architektur im Stream Wozu formale Methoden? mit Lars Hupel
Apr 28, 2026
Lars Hupel, Chief Evangelist bei Giesecke+Devrient und Co-Kurator für formale Methoden, erklärt Grundlagen und Einsatzfelder formaler Methoden. Er spricht über Theorembeweiser wie Isabelle, Model-Checking, Abstraktionstricks für große Zustandsräume und Pragmatik bei Kosten-Nutzen-Entscheidungen. Praktische Tipps: TLA+, funktionale Modelle und wie formale Modelle als klares Kommunikationsmittel dienen.
AI Snips
Chapters
Transcript
Episode notes
Statische Typen Erleichtern Verifikation
- Statisch typisierte Sprachen erleichtern Verifikation, weil viele Fehler schon im Typsystem auffallen.
- Sprachen wie Rust/Haskell bieten stärkere Typsysteme; Typsysteme allein garantieren aber keine inhaltliche Korrektheit.
Sortierbeweis Als Anschauungsbeispiel
- Lars erklärt Theorembeweiser am Beispiel einer Sortierfunktion: Implementieren, Theorem formulieren, dann Schritt-für-Schritt beweisen.
- In Isabelle schreibt man Implementation und getrennte Beweise; der Kernel prüft jeden Beweisschritt.
Kosten steigen Mit Formalität
- Höherer Formalisierungsgrad ist teuer: grobe Faustregel bis zu zehnmal mehr Verifikationscode als Implementationscode.
- Daher lohnt sich Proof-Aufwand nur in Domänen mit hohem Risiko oder hohen Kosten bei Fehlern.