> Tests and types can be complementary but this is not always the case. I never said it was? > If you use a language with dependent types you can prove that y

> Tests and types can be complementary but this is not always the case. I never said it was? > If you use a language with dependent types you can prove that your functions are correct Yes, for certain values of "prove" and "correct". Even if we ignore the cost of figuring out the proofs, it can be tricky to encode our mental models into formal statements. Automated tests are useful for checking the correctness of our implementation and our specification. > making tests redundant Not at all, in the same way that lorries don't make bicycles redundant. In fact, I like to use dependent type checkers to run my tests, e.g. test_Foo : Bool test_Foo = foo bar > 0 run_Foo : Equal test_Foo True run_Foo = refl This way, automated tests are run as part of the compilation process; and the build will fail if any of the tests fail (we can also use fancier encodings than Bool, to get nicer error messages, etc.).