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.