> We need a better C++ ("systems") base language that could have an optional borrow checker or bounded model checker enabled.

Are you describing Rust?