Its difficult for all programmers. The tooling still isn't there.

Try verifying the correctness of a JavaScript program with model checking. It won't work. Or try verifying correctness with abstract interpretation. For any sound system the output will just be "Top".

We have very deliberately developed technologies that enable rapid development. For "make it so a little message appears on the screen saying what day it is" features this works very well but it means even our formal analysis methods fall over on dynamic languages with heavy framework use.

This isn't just laziness. I'm a hardcore PL person and even I think that soundness is largely a mistake when making real analysis engines.