Type systems prove things about your programs.

Typeful programmers don't seem to see types the way Common Lispers or C programmers do. Instead, type systems are how you can partially prove the correctness of your program.

Thinking of types as proof systems offers several useful intuitive analogies. It is not just more rigorous testing; it's in a whole other universe from testing. Scientifically, we don't accept a hypothesis that seemed to work when we tried it with a few different things, we demand proof, which is qualitatively different.

Taking the time to prove your program's correctness may take more time than simply writing the program in many cases. (This is a complex issue I will return to later.) However, even in those cases, the benefit of the rigor of proof may outweigh the cost.

It may be that, when you are writing a program, you can intuitively see that your program is somewhat correct, but you don't know how to prove it. Well, if you can't prove it, should you, or anyone else, really trust your intuition? If you do prove it, no trust is necessary; all you need to do is trust the proving framework, the type system, to disallow nonsense, and the fact that the type system passed the program is enough to satisfy everyone that the proof is sound, so far as it goes.

Finally, type inference is “proof assistance”. Typeful compilers come with both proof checkers and proof assistance, but these, again, deserves separate posts.

Accordingly, I will often use the language of “proof” when talking about using type systems.