I think you're taking offense on behalf of Java when the paragraph is dragging Haskel and Rust.

Is it? When was the last time you saw Coq in the wild? If you ever saw it you can be certain the program is correct, but...

Clearly type systems live on a spectrum with varying degrees of sacrifices made, with each sacrifice compromising some ability to check for correctness, but giving back some other advantage, improved developer productivity being one possibility.

It is not a question of static typing or not – it is how complicated of a type system do you really need? Even Grug agrees that dynamic typing is not sufficiently complicated, but maybe a static type system that falls somewhere around the middle of the spectrum that helps catch the most grievous of errors (and provides popup magic!) with a sprinkling of automated testing to fill in the gaps where the type system falls short is best for the vast majority of programming situations?

There is a difference between Coq and say Haskell, for example. I guess I will disprove your entire point by finding an unknown dynamic language that nobody uses then.