Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.
On Tuesday, March 26, I’ll be giving a talk on propositions as types to the Lambda Zagreb Meetup group. The talk will be in Croatian and it is titled ¬ sve za ∀ (no ∃ uvod u propozicije kao tipove), which can be translated as ¬ everything is for ∀ (but there ∃ an introduction to propositions as types). Obviously, I incorporated logic operators into the title with the goal to make it catchy and to attract more audience with an unusual title. Given that only about 10 people RSVPed so far and that there are only three days left until the talk, it looks like I’ve achieved quite the opposite!
I applied to give a theorem proving seminar at a university. They chose Philip Wadler as a lecturer over me. That must have been close! Still, so disappointed…
To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.
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.