[qsort]

> 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.

[valenterry]

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

If you define useful by "we know that the compiler will finish in finite time" then I agree. And that's indeed a good point! In practice, there will always be runtime tests, at least for how long any of us and our children will live. :)