>In other words, the core, commonly identified “hard part” of Rust - ownership and borrowing - is essentially applicable for any attempt to make checking the correctness of an imperative program tractable. So trying to get rid of it would be missing the real insight of Rust, and not building on the foundations Rust has laid out.

Sure, but people wanting a smaller Rust might not care about the "real insight of Rust", but of the surface syntax, speed, apis, tooling (e.g. cargo), and so on...

I'd like a Rust like language that's GCed for example, and drops all the lifetime annotations and so on...