One thing is true: if you're not proving correctness of your code -- formally or informally -- then you are living in entropy and at very high risk of inefficiently delivering value through software. Knowing how to call "correct" on code is paramount.
And also -- yes, static type systems allow for (partial) machine verification of these proofs.
The missing piece is the innate -- and immense -- cost in having to express these proofs formally in a machine-checkable way.
Static type enthusiasts typically downplay these costs but they are simply wrong. I am not talking about the cost of learning how to code in a statically typed system--that should never be factored in. I am talking about the innate costs of formal verification (and strong static typing) that even the expert static typers pay. I have seen these guys work and they are delivering sub-optimally in time compared to the alternatives. Period.
I have been around the block with both static and dynamic typing systems and the latter by far optimizes for delivery throughput over time.
Formally proving correctness of your program has the upfront cost of formalizing the proof (to the degree required by the verification system) as well has having the effect of crystallizing your code in its current representation which makes it more difficult to (re-)factor for future uses.
Some of the (more reasonable) strong static type enthusiasts will concede that this kind of machine/type-proving is better done when the domain and code stabilizes. My hats off to these people for at least being honest about things.
However the next realization is that once code and domain stabilize the need/value for machine proving correctness (in typical business/data applications) drops substantially (for obvious reasons).
So the pragmatic value of strong type systems and formal verification is far lower than the proponents will have you believe. Of course we've known this truth forever but our industry forgets pretty quickly. Haskell and variants are on the rise in popularity; but make no mistake, if you are optimizing for overall delivery throughput over time -- even experts are swimming upstream with these languages.
Of course every time I point this out on HN I get downvoted -- but it kills me to think that a next generation of programmers are being misled down a path of formal purity with misrepresentative claims about the cost of using these tools in real business applications.
Just to dispel any idea that what I'm saying is philistinic, I am a mathematician/academic first, enjoy category theory, have written more than my share of academic proofs (including novel results), and think these tools are immensely fascinating.
But having been in industry now for 20+ years shipping web-scale and distributed data systems for business industries (what 90+% of us are doing, I imagine), where time is the most precious resource, I know with certainty that leaning on formal verification techniques (including strong static type systems) is an enormous tax compared to the alternative. That these tools work against fast-paced, iterative development.
It has also become evident to me that there is a vanguard of static type enthusiast who are not admitting (or perhaps do not understand) the relative cost of the pursuit. Who will point to a few null pointer errors (that, mind you, could be eliminated or reduced by other defensive coding techniques besides formal proofs) and use these to justify the herculean cost of their formal system.
If you're a junior or on the fence about static type systems - at least code in a weakly typed PL in which you can lean in one way or the other. If business outcome/throughput is what you value first and foremost, I guarantee you will gravitate more and more toward dynamic evaluation - especially as you realize the world of real business delivery produces constantly changing requirements and carrying out delivery in the face of purist formal modeling and proofs will be a substantial drag on what you can do for little relative benefit downtream.