5 ms·

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/18

by _fz 6y ago

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/18dda7f45541d2e8f47c351d72a20a25d3bfb4be/GameOfLife.agda#L95 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 6y ago
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 6y ago
  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.