Agreed, although I'd go a step further. A mutable variable has a type of reads and a type of writes. They vary in opposite directions. If you constrain them

Agreed, although I'd go a step further. A mutable variable has a type of reads and a type of writes. They vary in opposite directions. If you constrain them to be the same then they must therefore not vary at all.