Earlier quoted context omitted.
> But is it wrong? Yes, because people don't "not often ship code in statically typed languages". It's obviously wrong.
Is it? When was the last time you saw, say, Coq in the wild? If you ever saw it you can be certain the program is correct, but I certainly have never seen it. Most likely because anyone using it really is still trying to satisfy the type checker. 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…
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.