This is both a straw man and a fallacy. Nicely done.
Also something I never claimed.
You are basically saying that since you can't prove a program can be 100% demonstrated to be correct, there's no point in trying to approach this goal, therefore dynamically typed languages are good enough.
With your reasoning, we wouldn't be using safety belts because they can't guarantee you'll survive a car crash 100%.
Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types, which is why we see dynamic languages converging toward static typing and never the other way around.
In ten years from now, we'll look at dynamically typed languages as "It looked cool at the time, but we know better now". A bit like we look at FORTRAN and COBOL today.