I’m excited to see how this works out in practice. The nice thing about linking lifetimes to lexical scope is that it’s easier to see the lexical structure of a program than to reason about its control flow. But if people have an intuition for the control flow that tends to match reality, this could be fine.

Looks lexical to me, if we just add braces:

  fn main() {                               // SCOPE TREE
                                          //
    let mut names =                       // +- `names` scope start
        ["abe", "beth", "cory", "diane"]; // |
                                          // |
    let alias = &mut names[0];            // | +- `alias` scope start
                                          // | |
    *alias = "alex"; // <------------------------ write to `*alias`
                                          // | |
    println!("{}", names[0]); // <--------------- read of `names[0]`
                                          // | |
                                          // | +- `alias` scope end
                                          // +- `name` scope end
  }

That is to say:

  fn main() {                               // SCOPE TREE
                                          //
    let mut names =                       // +- `names` scope start
        ["abe", "beth", "cory", "diane"]; // |
                                          // |
    { let alias = &mut names[0];            // | +- `alias` scope start
                                          // | |
      *alias = "alex"; } // <------------------------ write to `*alias`
                                          // | |
    println!("{}", names[0]); // <--------------- read of `names[0]`
                                          // | |
                                          // | +- `alias` scope end
                                          // +- `name` scope end
  }

If that can be made to work without diagnostics, it's a better solution than playing games with de facto tying scopes to the last uses of identifiers.