For the read case, do you mean that in nonbranching code, a read can be considered a destroy+create that cancel out? How is that legal if the reads are also writes into other variables, or copied into an array/tuple and returned to a caller? That seems a clear violation of linearity.

Also, that doesn't seem true for branching structures, but I guess technically in an immutable language loops iterations are recursive functions.