No. CHERI doesn't help with data races, for example. Also it doesn't help with compiler optimizations that exploit UB to make code faster. Unfortunately low le

No. CHERI doesn't help with data races, for example. Also it doesn't help with compiler optimizations that exploit UB to make code faster. Unfortunately low level languages are kind of addicted to optimizations that only work for languages with UB. There's too much performance being left at the table if you create a programming language entirely without UB. There's no law of nature, however, that says this must be the case forever. You could have a theorem prover prove useful properties about programs (and them feed them to the optimizer) and refrain from "optimizing" if you can't 100% prove that this will not break.