It is no surprise. They can be coerced to prove your program correct, negating the need to do unit tests.

But this is only true for certain languages. Overall most type systems are not Turing complete and therefore not suited for general computation