The second notion, where it's clear that the memory space can safely be used, is why there's interest in linear and affine type systems. These systems describe

The second notion, where it's clear that the memory space can safely be used, is why there's interest in linear and affine type systems. These systems describe types whose value can only be read one time, and for linear types, which must be read one time. On the surface that can seem a bit stupid, but the practical outcome is that compilers can determine when an array's contents can be mutated in place rather than overwritten. A variable you read over and over can be thought of theoretically as one you duplicate, then read one copy of. Since the act of reading the copy destroys it, a compiler implements this by merely reading the value directly. Passing an array into a subroutine however means the compiler either copies it, or forbids further access after passing it in. If it's the latter, the memory space is available for re-use inside the subroutine. Rust uses affine type theory for its borrow system to provide memory safety. Function language research is looking at linear and affine types for a variety of applications including performance.