> is not inclined to prove it (as represented by coding type checking or other handling)
This is known as a reachability problem that in the general case cannot be proven. So, "not inclined" may actually mean "can't (in any reasonable amount of time)".
It's not "in any reasonable amount of time". Proving in the general case whether a variable is unused in code or not is equivalent to solving the halting problem. This follows from Rice's theorem:
Yes, but it's more nuanced than that. Even if you can prove that a computation always terminates you can't necessarily prove that it yields the wanted result in any reasonable amount of time. This is the bounded halting problem, and it applies even to languages that only allow terminating computations. In those languages, the halting problem is nominally gone, but the bounded halting problem is just as bad as for Turing-complete languages. Just how bad is it? It is a time complexity class that includes all time complexity classes, i.e. it is harder (in general) than any problem that is computable and known to complete within f(n) steps, where n is the size of the input and f is any computable function.
I came to say much the same thing, but even take it a step further and point out that proofs are subject to human error as well. More powerful programming constructs are a great tool, but at some point it's turtles all the way down. The Knuth quote comes to mind: "Beware of bugs in the above code; I have only proved it correct, not tried it."
