[a_imho]

This is not the same problem AFAIU. You don't know whether your tests encode the correct specification either, but you must run them first to find out whether they pass, but with (dependent) types you can have the sorted list property encoded in compile time, but still can't be sure whether it is correct.

[_fz]

I recently implemented Conway's Game of Life in Agda. I still had to write "test cases" to get the whole thing right: https://github.com/fzipp/agda-life/blob/18dda7f45541d2e8f47c...

Sure, they are validated at compile time because they are propositions as types, but in the end they are still basically test cases: expected output for a given input, and the compiler is the test runner.

I don't know how to encode the full "Game of Life" property as dependent types, I am still an Agda newbie.

[valenterry]

In this context, I think we should not call them "tests" to not mix them up with "runtime tests". Even though they are indeed tests in a sense

[_fz]

Sure, I don't know what the correct term is. But I personally did not really gain anything from the type system that helped me get the logic of the program right. Whether a Turing complete type system "runs" my assertions at compile time, or a test runner does it on save does not make a difference to me. Actually, I could measure the compile time for this simple one-page program in seconds, while the Go tools compile and test a Game of Life implementation in a fraction of a second.