But, as you surely know, types prove something about a piece of code. This means they can very well prove the absence of (certain) bugs.

So generally, the more invariants you manage to capture in your types, the more categories of bugs you can statically prove will never happen.