Static type systems (particularly explicit rather than inferred ones) have multiple goals: as a form of documentation; as a way of specifying interfaces so pieces can be more reliably developed independently because the seam isn't just in documentation or peoples' heads or a bunch of unit tests; as a way of designing an app (when program = data + algorithms, some people like to start with the shape of the data); and finally as a way of proving more things about the code.

I'd submit that the historical actual use of types doesn't emphasize the proof nature of types nearly as much as academic CS does. Unsound type systems are common in practical languages. And I believe that isn't accidental: because, with all the other things types are used for, you need an expressive type system, and that in turn means it is either going to be complex and sound, or simple and unsound (i.e. with escape valves like typecasting and runtime type errors - I'm considering compile-time type analysis only).