This is a really good question! Basically a lot of properties that you probably can think of that could be checked for but aren't expressible in Java types sys

This is a really good question! Basically a lot of properties that you probably can think of that could be checked for but aren't expressible in Java types system can still be expressed using types in another system. Therefore if you want something more powerful than the types your using, use more powerful types! It turns out that we do not really need more to reach the limits of what we can check for automatically.