Those facts are untrue. If i am using a sound static type system, I have a formal way of modeling and understanding what will happen to my program, even without tests.

If a function has been statically proven to return an int, I know it will either return an int or not return at all. It can't suddenly return a hashmap at runtime, no matter what untested state it enters.