Types and Proofs

Posted on November 14, 2017 by Marko Dimjašević

Courtesy of Ella’s Dad

I found a powerful analogy between software correctness and dishes:

Testing is washing the dishes. Automatic tests are a dishwasher. Types are proof that your dishes are not even dirty.

In a discussion thread that the analogy opened, there was a clarification stating that you cannot prove other than what is stated in a theorem:

Type-checking proves that your dishes do not have particular sorts of food stuck to them. They may still be dirty.

That is, if your type does not have a particular property, then the property cannot be proven by a type system. For example, if you use an integer type to describe the result of a function computing the factorial, then the type obviously does not state that the factorial is a non-negative integer. Choosing a less precise type (or even no type at all!) over a more precise type is a missed opportunity to have one more proof in your program.

If this dish talk got you confused, read up on the Curry-Howard correspondence.