Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.
Idris is a pure functional programming language with dependent types. In this post I am giving an example by David Christiansen on proving a parity theorem (or property) in Idris. The theorem states that every natural number is either even or odd. The example below demonstrates how to do theorem proving with a functional programming language such as Idris. It relies on equality expressed at the type level, which is possible thanks to dependent types. With that, Idris stands in stark contrast to languages such as Scala, where equality is broken. In the example, allEvenOrOdd k is a proof for every natural number k.