> But on a more theoretical level, OP is right: you _can_ save the tests with, given a powerful enough typesystem.

Yes and no. The trick is building a type system simultaneously strong enough to encode the properties you want, and weak enough that it's statically decidable.

There will always be properties you can't encode in a (useful) type system.

It's a fine line to walk, really. There's an argument to be made that most of the times we don't actually need Turing-completeness, and we'd better off using only types to encode computations, but OTOH I don't really want to think about what coinductive types I must define to solve a problem that could be solved with five lines of javascript instead.