That's absurd, I'm not arguing anything of the sort.
If you want an analogy, I'm arguing that a condom helps prevent STD's and unwanted pregnancies. It isn't perfect, but at least it is better than not wearing a condom at all. Nobody loves wearing a condom, but we do it cause it is the right thing to do.
You can't prove away chlamydia or an unwanted pregnancy, but you can provably eliminate whole classes of logic errors by having more powerful type systems.
100%. Compilers for the win for sure. It was a big reason why I started to write Java code and move away from PHP. This lead me to co-found Java @ Apache.