I suppose it's because a proof is contained within itself while a computer program may interact (in this case with another component within the same application

I suppose it's because a proof is contained within itself while a computer program may interact (in this case with another component within the same application) in non-obvious ways. Clarity in variable names helps to prevent this behavior, although it doesn't completely eliminate the risk.