In dieser Folge spricht Richard Seidl mit Michael Sperber und Markus Schlegel über formale Methoden der Softwareentwicklung. Sie erklären, warum Mathematik und Spezifikationen ein solideres Fundament liefern als typische Testverfahren. Besonders anschaulich wird es, wenn sie die Vorteile funktionaler Programmierung diskutieren und zeigen, wie sich Softwareeigenschaften beweisen lassen. Praktische Einblicke in Typsysteme, Beweisassistenten und Property-Based Testing machen das Thema greifbar.
Highlights:
- Funktionale Programmierung macht Software beweisbar, weil x = x + 1 mathematisch Unsinn ist.
- Formale Methoden sind nicht aufwendig – sie sind effizienter als imperatives Debugging.
- Property Based Testing ist der Einstieg: Spezifikation mit Allquantoren statt vier Beispiele.
- EU-Normen verlangen Beweise, nicht Tests – C-Code wird aus verifiziertem funktionalen Code generiert.
- Typsysteme beweisen bereits Eigenschaften – Dependent Types erweitern das auf ganze Spezifikationen.
((um das Video zu sehen, muss in den Cookies den Statistiken zugestimmt werden))
