To add some color here on the difference between a type proof and a test: consider that you can never test all possible strings for reverse. However, a type pr

To add some color here on the difference between a type proof and a test: consider that you can never test all possible strings for reverse. However, a type proof can show that reverse, reverses all possible strings. It is possible to test that a function on 16 bit integers returns the correct value for all inputs. Doing so would be a proof by exhaustion. Type based proofs let us prove things using other methods than exhaustion, which is the only possible way to prove things with tests. That is an important property.