I think under the constrained of not using GC and not defaulting to unsafe memory that the borrow checker is a decent design. The constraints mean that you need

I think under the constrained of not using GC and not defaulting to unsafe memory that the borrow checker is a decent design. The constraints mean that you need some form of formal verification of your lifetimes. These can get very complex and difficult to use. So it might make sense to limit their expressiveness and instead rely on unsafe escape hatches. I think Rust's borrow checker provides a decent tradeoff between easy of use and how often unsafe is needed. There are rough edges and progress has been slow, but I have yet to see anything radically better. Other system PLs require a lot more unsafe usage (e.g. Zig) and I'm not aware of any mainstream system PLs that offer much more expressive verification.