>memory safe (without a borrow checker) This sounds like a very weird statement. In my opinion, a proper proof-oriented language would inevitably contain a bo

>memory safe (without a borrow checker) This sounds like a very weird statement. In my opinion, a proper proof-oriented language would inevitably contain a borrow checker variant as a subset of its functionality (assuming the language has notion of pointers/references and focuses on achieving "zero cost abstractions"). Lifetime annotations and shared/exclusive references provide essential information and code use restrictions which enable automatic proof generation. After all, type and borrow checkers are nothing more than limited forms of automatic proof generation which are practical enough for wide use.