When I say adequately tested, I mean much more than unit tests. Unit tests aren't going to give you bulletproof code. They don't detect bugs that arise from interactions at a higher level.

An arbitrarily complex type system, with dependent types, could detect any bug, since it's formally equivalent to requiring the program be proved correct. But using such a type system is so onerous that I don't know anyone who realistically does it in production.

If you wrote such types, you're basically giving a formal specification of what the program is supposed to do. That could then be used, and likely much more easily, for high volume property-based testing.

Unit tests and types solve somewhat different problems. You can force a unit test to check everything a type system does with effort (mostly by throwing wrong types at your API and verifying you get an error), but I'm not sure how you would use the type system to enforce sort() actually sorts. Sure sort can take a listOfFoo and return a sortedListOfFoo - but that doesn't verify sortedListOfFoo is actually sorted - and in many cases I want an API that is find with listOfFoo but should handle sortedListOfFoo as well.

With dependent types you can encode any proposition in first-order logic (?). You can indeed define an array type that is necessarily sorted. It won't be pretty but it's possible.

More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

I like type systems as much as anyone but I can't see how your type system will check that sin(pi) == 0

if you have a type system expressive enough to do things like that, you've basically got another turing-complete layer on top of your existing language, which is itself ... dynamically typed.