I'm of the opinion that type systems as commonly found confuse several things:

• Compiler optimizations.
• Memory size and locations.
• Position in a class hierarchy.
• Supported behavior.

Of those, only the second and fourth have much to do with program correctness. Even then, there are too many other things that can go wrong — suppose you implement the Serializable interface in a Java class but code a method body incorrectly. Even static analysis of the code can't catch logic errors.

A well-written test suite can catch those kinds of errors. You'll never get around that with a compiler. It's up to you if the price to pay for static types is worth the things it can possibly catch.