Yes, we will never be able to prove that a program is 100% correct but that doesn't mean we shouldn't prefer solutions that bring that number up (statically typed languages) over solutions that don't (dynamically typed languages).
Just because you can't do something perfectly doesn't mean you shouldn't try to do it as best you can.
In the real world, it may well be the case that while you're screwing around with a baroque type system, your competition has iterated three or four times and your milkshake has been drunk.
Of course your compiler will never be able to proof the correctness (or lack of it) of all programs.
The relevant question is, what share of useful programs can our compilers help us creating? This is not answered yet, and you seem to have never even thought about it.
Erlang is reliable because it's fault tolerant. The Strong Static Typing camp wants software that is reliable because it is faultless.
Elixir has Erlang's philosophy on the problem. I think most of the wailing and gnashing of teeth is because most languages (even most statically typed ones historically) have just completely punted on the notion of language support for writing software that doesn't fall over in a stiff breeze. The more we build layers of software between humans and their actual goals the more this is going to come to a head.