The SPARK subset of Ada^1 has a similar kind of move semantics for pointer types^2. 1: SPARK is a formally verifiable subset of Ada: https://en.wikipedia.org/w

The SPARK subset of Ada^1 has a similar kind of move semantics for pointer types^2. 1: SPARK is a formally verifiable subset of Ada: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) 2: https://arxiv.org/pdf/1805.05576 https://arxiv.org/pdf/1805.05576