[electronvolt]

So it turns out you can basically use type theory to encode a surprisingly large number of desirable traits about your program. (Caveat being that as you get more restrictive, you reject more "good" programs at compile time--no free lunch with Rice's theorem.)

For example: In this paper, they basically use types (with an inference algorithm) to catch kernel/user pointer confusion in the Linux kernel. (https://www.usenix.org/legacy/event/sec04/tech/johnson.html)

It turns out you can encode a lot of other interesting properties in a type system (esp. if you're building on top of the existing type system), though--you can ensure that a java program has no null-dereference checks (https://checkerframework.org/ has a system that does this), and Coq uses its type system to ensure that every program halts (as a consequence, though, it isn't actually Turing complete).

There's also cool things like Lackwit (http://ieeexplore.ieee.org/document/610284/) which basically (ab)used type inference algorithms to answer questions about a program ("does this pointer ever alias?", etc.).