More like you're arguing that there is no baby in the bath you want to throw out. Coming back to your previous comment: > This (i.e. proving a variable is ne

More like you're arguing that there is no baby in the bath you want to throw out. Coming back to your previous comment: > This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.