3 ms·
Tests and types can be complementary but this is not always the case. If you use a language with dependent types you can prove that your functions are correct,
by AnaniasAnanas 8y ago
Tests and types can be complementary but this is not always the case. If you use a language with dependent types you can prove that your functions are correct, making tests redundant.
- machiaweliczny 8y agoCan you recomend some good language with depended types to try?
- AnaniasAnanas 8y agoAgda if you want to write proofs, Idris if you want to write programs. There is also Coq which is more popular but I would not suggest it to a beginner. (note: both Agda and Idris can be used for both proofs and programs, it's just that each have their own focus)
- chriswarbo 8y ago> 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.).