This is wrong. For example, capabilities and typestate are the sorts of things that non-Rust languages are sometimes able to use to control the order in which things can be used. Imagine this sort of thing (I'm going to use Rust-like syntax and visibility rules, but imagine that this isn't Rust):
pub struct Singleton { … }
struct S1; struct S2; struct S3; /* not public */
impl Singleton {
pub fn new() -> (Self, S1) { … } /* panics if called more than once */
pub fn method_that_must_be_called_first(&self, S1) -> S2 { … }
pub fn method_that_must_be_called_second(&self, S2) -> S3 { … }
}
This controls the order in which the methods of (the only) Singleton can be used by controlling access to S1, S2, S3 values – if the language's type system doesn't have Contraction then the methods must be called in order, and even if it does have Contraction then the first call to each of the methods still has to happen in order. This is done entirely with types, rather than the order of contexts in typing judgements (in fact, I don't think removing the Exchange rule would even be useful to try to implement this sort of ordering requirement). I wrote this to control the order of method calls, but you can do the same sort of thing to control the usage of variables, too (but you have to give each of the variables a different type, because it's a type-based method of enforcing order).
You are using "lifetime" in your post in a way which doesn't match the way that the word is used in Rust. In Rust, a lifetime is a property of a borrow, not an object. For example, borrowing an object isn't enough to allow you to use that object after the borrow ends, even if the object itself has not been dropped yet. Likewise, there are some ways to create a place which lasts throughout the entire program execution and never drops (e.g. Box::leak()) – it is possible to move objects in and out of such a place even though it is not itself a free variable in the typing judgement at all (it's accessed via a mutable borrow, but the value in it continues to exist even if the mutable borrow is dropped). A system for limiting moves should be able to limit moves in and out of a leaked box, but the Exchange rule is unable to do that because it is not a free variable.
There are plenty of other things that Rust can do that your model doesn't handle well (the following code is Rust, this time):
let a = vec![1];
let b;
if some_condition() { b = vec![2]; }
let c = vec![3];
if some_other_condition() { b = a; a = vec![4]; }
dbg!((a, c));
This sort of conditional initialization / conditional dropping isn't expressible using an ordered context in the type judgement because type judgements have to be statically known at compile time. For example, you don't know at the time when a is declared whether the value in it will be dropped before or after c.
(Interestingly, there's one aspect in which Rust does care about the order in which variables appear statically – at the end of the function, the destructors of the values currently in c, b and a will run in that order, except that b's destructor won't run if it was never initialized. Notably, this order isn't affected by moves, so in the case where Rust does care about declaration order, moves don't change the order and thus aren't interacting with the Exchange rule.)
As another example, consider a simple sorting routine like this:
fn selection_sort<T: Ord>(array: &mut [T]) {
let mut suffix = array;
while suffix.len() > 1 {
let mut min_pos = 0;
for i in 0..suffix.len() {
if suffix[i] < suffix[min_pos] { min_pos = i; }
}
let (first, rest) = suffix.split_first_mut().unwrap();
if min_pos > 0 {
core::mem::swap(first, &mut rest[min_pos - 1]);
}
suffix = rest;
}
}
To work correctly, this relies on being able to swap elements within the array it's borrowing. But the array has an unknown length and it's represented by just a single variable in the typing judgement – so the swaps can't be something that are visible within the judgement because the judgement is the same before and after the swap. (It has to be – the swap is conditional and won't always happen.) Likewise, the swap is in a loop, but typing judgements have to be the same at any given point in the program, including every iteration of a loop. The selection_sort function should work only on types T that are moveable and overwritable, but trying to enforce that by deleting the Exchange rule doesn't work.