something i'd like to see in a borrow checker (which i think causes problems in rust, because of the "leaking is safe" thing. which sounds like it could be a difficult hole to plug in language design):
in rust, &mut means "this pointer points to an initialized value, and will point to an initalized value at the end of scope"
i wish it also had &in, &out, and &tmp, for "initialized->uninitialized", "uninitialized->initialized", and "uninitialized->uninitialized"
Their intra-function behaviour seems difficult to define for non trivial cases. For instance a &tmp would need to be write only until it’s written to, then it can be read from as well, but it needs to be consumed before its scope ends, transitioning back to a write only reference. So you’d need a type system which can transition parameters through typestates (is that a subset of effects systems or unrelated?).
What you're describing is exactly correct - you need a more robust "typestate" system (I call them "annotations"). Most languages have typestates - where you can, for example, declare a variable without immediately assigning it a value, but that variable remains write-only until it is assigned to.
But these typestate systems aren't very elaborate usually. I've recently been doing research on the (hypothetical) design of a language which has typestates that can cross function boundaries - you can call a function that annotates that it uninitializes one of its arguments, and then that reference you passed in is now considered uninitialized in your local scope.
in rust, &mut means "this pointer points to an initialized value, and will point to an initalized value at the end of scope"
i wish it also had &in, &out, and &tmp, for "initialized->uninitialized", "uninitialized->initialized", and "uninitialized->uninitialized"