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.

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

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.