Comment
Comment by waynecochran
This (i.e. proving a variable is never used) is impossible in general
since it is equivalent to the halting problem.
There are many cases where it can be solved, so the compiler lets the programmer
get away with this in the cases where one of the mutable borrows is provably not used. Now imagine re-factoring the code so that the compiler could no longer produce the proof. Now an error is generated and the programmer is left scratching their head
wondering where this new error came from.