“Program testing can be used to show the presence of bugs, but never to show their absence” -Edsger Dijkstra
One of the best things about moving from being a technologist working in an investment bank, to transitioning into the world of small business ownership as Director & CTO of an established IT recruitment firm, is my surprising exposure to new tech. It stands to reason in hindsight. It can be easy to get siloed with tech working in a very specific area of a bank, with commonly available and often mandated toolsets.
Moving out of corporate to take on this exciting new challenge, it’s been quite an eye opener to see how other firms and industries adopt a range of technology tools to solve their business challenges.
Take Coq as an example. Heard of it? Certainly, new to me, as I entered into an initial conversation with an important client here in London. However, I’ve been able to quickly bring myself and the team here up to speed on this interesting technology. So, in the first of a series of #liveandlearn blogs, I want to share more with you around little known, but highly powerful tools, like Coq and Agda, which are important weapons in some of our clients’ technology stacks.
Coq & Agda are various flavours of “Proof Assistants” - more commonly known as “Interactive Theorem Provers”. Great… but what’s a Theorem Prover, how is it applicable in software development and why would this client be looking to build out that skillset? I was motivated to find out more, not just to satisfy my own curiosity, but also so that the team here could properly get their hands round the tech in order to secure our success in finding and qualifying the best talent for this client.
Theorem Provers are a different way of testing your software, but unlike traditional methods where you compile countless unit tests, coupled with various layers of integration & scenario tests hoping you’ve covered all edge cases. With a Theorem prover, you can prove the absence of bugs as it gives you a method for mathematically proving the correctness of your functions.
They allow you to specify your function and an associated proof that asserts its correctness using mathematical concepts like simplification, reflexivity etc.
Still confused? Let’s take an example of defining a function that given a day of the week returns the next working day and see how this works.
First, we define the data type:
Inductive day : Type := | monday : day | tuesday : day | wednesday : day etc..
Having defined day, we can write our function:
Definition next_weekday (d:day) : day := match d with | monday ⇒ tuesday | tuesday ⇒ wednesday | wednesday ⇒ thursday | thursday ⇒ friday | friday ⇒ monday | saturday ⇒ monday | sunday ⇒ monday end.
Now traditionally you might write various test case assertions, for example:
Example test_next_weekday: (next_weekday (next_weekday saturday)) = tuesday.
But what Coq allows you to do is use this example declaration to verify the correctness of the function by simply doing the following:
Proof. simpl. reflexivity. Qed.
This effectively says that both sides of the example equate to the same thing after some simplification and reflectivity.
What’s really cool about Coq is that once it’s proved the correctness of your function you can ‘extract’ into another more conventional programming language like Haskell, with a high-performance compiler so that you’ve now got a proved-correct algorithm compiling into efficient machine code that you can execute with confidence. That’s something to crow about!
And how did Coq get it’s name? Well, firstly the logical framework off which it is based is called “Calculus of inductive Constructions” and it was developed in France where in some groups there is a tradition of naming development tools after animals. In this instance they've gone with the French name rooster 'Coq'.
Useful Links for Further Reading:
Coq Software Foundations (I recommend volumes 1 & 3)