Wie Mathematik aus deinem Code bombensichere Software macht

🚨 Testen wir manchmal eigentlich zu viel? Viele Tests heisst nicht, dass auch viele Fehler gefunden werden. So können wir das lösen: Kostenloser Online-Workshop

„C und C++ sind die gefährlichsten Programmiersprachen auf der Welt, ausgerechnet für die Systeme, von denen wir wollen, dass die richtig funktionieren." - Michael Sperber

In dieser Episode spreche ich mit Michael Sperber und Markus Schlegel über formale Methoden – die vielleicht unbekannteste und gleichzeitig mächtigste Technik, um Software wirklich korrekt zu machen. Während wir beim Testen oft nur ein paar Beispiele prüfen, ermöglichen formale Methoden Software mathematisch zu beweisen, dass sie für alle möglichen Eingaben das Richtige tut. Die beiden zeigen, warum funktionale Programmierung der Schlüssel dazu ist, wie Property Based Testing der erste praktische Schritt sein kann und weshalb dieser Ansatz nicht nur sicherer, sondern oft sogar effizienter ist als klassische Entwicklung.

Dr. Michael Sperber ist Geschäftsführer der Active Group GmbH, die Individualsoftware ausschließlich mit funktionaler Programmierung entwickelt. Er ist international anerkannter Experte für funktionale Programmierung und wendet sie seit über 20 Jahren in Forschung, Lehre und industrieller Entwicklung an. Außerdem hat er zahlreiche Fachartikel und Bücher zum Thema verfasst, sowie das Curriculum für das iSAQB-Advanced-Modul "Formale Methoden" (zusammen mit Lars Hupel). Michael Sperber ist Mitbegründer des Blogs funktionale-programmierung.de und Mitorganisator der Entwicklerkonferenz BOB.

Markus Schlegel ist Softwarearchitekt bei der Active Group GmbH. Markus hat 2013 die funktionale Programmierung für sich entdeckt und schläft seither wieder ruhig.

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.