Testing, Types, & Correctness

September 10, 2017

Understanding correctness of code really comes down to proving that the code does the right thing. What tools do we have as programmers for proving the correctness of our code?

  1. Unit tests prove that the code is correct for specific inputs.
  2. Type systems prove the absence of (certain kinds of) incorrectness.
  3. Theorem provers prove sophisticated claims about our code for us.
  4. Program authors can prove the correctness of their code (i.e., with a traditional pen-and-paper proof).

The first three are exciting because they involve a computer doing most of the work for us! That said, none of the first three are as universally applicable as the last: doing the proof ourself. Unfortunately, it’s also usually the most toilsome.

Note the double negation in (2). Type systems themselves don’t prove correctness, they prove that there aren’t certain kinds of incorrectness, namely: type errors. Meanwhile, unit tests are rarely (if ever) exhaustive. This is why testing and type systems are complementary—one is not a substitute for the other.

It’s important to both have strong testing practices and languages with disciplined type systems. The hardest part of writing quality software is ensuring that it runs without bugs. The more tools we have in our arsenal to combat incorrectness, the easier it is to write code for the long term.

ABTs in Haskell

I’ve been learning and using Haskell on-and-off for the past couple of years. One of my early complaints was that I couldn’t find a good library for working with variables and binding that used locally nameless terms. Recently though, I found unbound-generics, which checks all my previously unfilled boxes. Continue reading

Variables and Binding

Published on October 28, 2017

System Fω and Parameterization

Published on September 27, 2017