One can at least argue that types reduce the difficulty of machine
verification by providing guidance to the automated verifier --- proof
obligations generated by type checking can be verified in certain
stereotypical ways, or with well defined algorithms. The more of the
automated inference that one can move into the type system the greater
the level of automation in the verification overall. PVS has been
particularly aggressive in pursuing this philosophy.
In short, one can argue that there are very concrete pragmatic issues
surrounding the choice of a type formalism in a verification systems.
David