I'm not very familiar with Hylo, but I
think it's in the opposite direction from rust than what I'm suggesting.
I'm suggesting a language where there's no difference between Box<u32> and u32. &Vec<u8> and &[u8] are the same thing. I don't need to write Box::new(...) around my closures to pass them to functions that take a function pointer. This comes with overhead, but in exchange we get simpler less verbose code. I.e. a language that isn't systems level, and isn't particularly machine-empathetic. But still has all the lightweight-formal-methods power of rust with lifetimes and mutable vs shared borrows (and thus references to references) and so on.
My impression of Hylo is that it's purpose is to be a similarly low level systems language to rust, just with a less complicated, and as a consequence less expressive, lightweight formal methods system for proving correctness.
I agree I don't expect rust to be displaced anytime soon. It creates a lot of time to create a good compiler, and a lot more to create the ecosystem of code, tools, and community around it.