And you are falling prey to the Nirvana fallacy [1].

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.

[1] https://en.wikipedia.org/wiki/Nirvana_fallacy

I'm saying that you have to actually demonstrate that additional formalism adds value before you start claiming that it does.

Yes. Real-world programming is an entirely different thing from academic research.

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.

No point on citing this or the Halting Problem.

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.

fun fact: the Busy Beaver function applied to the universe yields a finite number and seeing as we need to leave some space to actually run the program we can conclude that in fact any program that can be written can be proven to halt. Granted that in case of "for(;;){printf("hello");}" that halt is the heat death of the universe but it's still theoretically tractable.