Re:Learn Go by writing tests – Hello, world (2018)
by valenterry on Friday March 12, 2021 @08:36AM
(#26435643)
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
Re:Learn Go by writing tests – Hello, world (2018)
by _fz on Friday March 12, 2021 @08:54AM
(#26435800)
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.
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.