Google Godel's incompleteness theorem.

In a nutshell, if you can mathematically prove a certain degree of soundness of your code, you have not done anything to show your code does what it is supposed to do.

Basically, you could be doing wasted work to satisfy your compiler, and have made zero progress in solving your problem, because that's not what the type system does.

Dynamical languages focuses on solving problems of human beings. The human beings' requirements are often inherently arbitrary, logically unsound, or even self-contradictory. Shoehorning a type system in there often serves to make solving human's problem harder. Consequently, in practice, most popular programming languages are dynamic. The current craze with types is just a fad, in my opinion.