Richard Seidl
Testing software usually means trying out a few examples and hoping that the rest works. Formal methods take a radically different approach - they prove mathematically that code is correct for all conceivable cases. Functional programming forms the bridge between mathematics and code because it works with equations instead of state changes. Property-based testing is the first practical introduction to this world before resorting to proof assistants.
Podcast Episode: Formal methods in software quality
In this episode, I talk to Michael Sperber and Markus Schlegel about formal methods - perhaps the least known and yet most powerful technique for making software truly correct. While we often only check a few examples during testing, formal methods allow software to mathematically prove that it does the right thing for all possible inputs. The two show why functional programming is the key, how property-based testing can be the first practical step and why this approach is not only safer, but often even more efficient than classical development.
"C and C++ are the most dangerous programming languages in the world, for the very systems of systems that we want to work properly." - Michael Sperber
Dr. Michael Sperber is Managing Director of Active Group GmbH, which develops individual software exclusively using functional programming. He is an internationally recognized expert in functional programming and has been using it in research, teaching and industrial development for over 20 years. He has also written numerous articles and books on the subject, as well as the curriculum for the iSAQB Advanced Module "Formal Methods" (together with Lars Hupel). Michael Sperber is co-founder of the blog funktionale-programmierung.de and co-organizer of the developer conference BOB.
Markus Schlegel is a software architect at Active Group GmbH. Markus discovered functional programming for himself in 2013 and has been sleeping soundly ever since.
Highlights der Episode
- Functional programming makes software provable because x = x + 1 is mathematical nonsense.
- Formal methods are not complex - they are more efficient than imperative debugging.
- Property-based testing is the entry point: specification with all quantifiers instead of four examples.
- EU standards require proofs, not tests - C code is generated from verified functional code.
- Type systems already prove properties - dependent types extend this to entire specifications.
Formal methods in software development: Why math makes our software better
What are formal methods actually?
Formal methods sounds complicated at first. It conjures up images of equations and proofs from school. But what are they really about? Michael Sperber explains that formal methods are mathematically sound techniques that help us to reliably prove certain properties of software. A concrete example: a speedometer in a car must always show the correct reading. It is not enough to check the speedometer with a few test drives. The EU wants to guarantee that the deviation remains within prescribed limits at all speeds. Such requirements can be formulated as mathematical equations and can be appraised using formal methods.
So instead of just testing individual examples, you describe exactly what the software must always fulfill. You then translate the software and the requirements into mathematics and appraisal whether they really fit together. This creates real proof that something is right.
Functional programming: more math in the code
Formal methods are often based on functional programming. But what is that actually? In languages such as C or Java, we tell the computer exactly how to do something. We don't just say "the result is like this", but give an exact step-by-step instruction. This makes it difficult to argue with mathematical precision.
Functional programming is different: here, we tend to describe "what is". Functions are like equations in mathematics. If the function is correct, the whole context is correct. Markus Schlegel believes that this means that the technicality, i.e. what the software is supposed to do, is immediately clear in the code - without the need for comments or extra documentation.
Programs in functional languages such as Haskell, F#, Scala or Clojure even make it possible to express many properties and rules directly and prove them mathematically later. This means you work closer to the mathematical methods and can better check whether everything works correctly.
Proofs for software: how it works in practice
Proving software sounds huge and complicated. Do you have to do weeks of math? According to Michael Sperber, it does involve some rethinking, but is often no more time-consuming than classic testing. Special tools - so-called proof assistants - are particularly helpful. They support the reliable and even somewhat automated implementation of the proof process.
The proof itself is usually stored in the code or in separate files. The tools then check with each software build whether the evidence is still valid - just like normal testing.
Property-based testing: the easy way to get started
There is a good intermediate step before you tackle entire proofs: property-based testing. This method comes from functional programming and has since found its way into many other languages. The idea is to describe properties that should always apply to all possible input data. The testing tool then automatically generates many different tests and checks whether the software behaves as described.
In this way, you can find many program errors without a complete proof and get used to the way of thinking of formal methods.
Why all this? And what do I need to get started?
Most people currently "only" test by example and hope that the code then runs correctly in all cases. But as Richie says in the interview, these methods are no longer sufficient for complex and safety-critical systems. That's why companies in the automotive and medical sectors, for example, are increasingly using formal methods - and it's worthwhile for everyone to take a closer look.
If you are curious, you can find a free introduction to the topic developed by Michael Sperber at deinprogramm.de. The ISAQB has also published a curriculum on the subject. Simple methods such as property-based testing can be tried out directly.
Formal methods are not just for freaks or researchers, but for anyone who wants to develop robust software. They help to raise software quality to a new, measurable level - and make everyday life easier and safer for developers and testers. Anyone who has ever experienced what it feels like to prove security instead of just hoping for it understands the value behind it. It's worth taking a closer look!