There is no such thing as "fundamentally impossible to do it safely": if you use a theorem prover like Coq then you can formally verify any* code as correct, no

There is no such thing as "fundamentally impossible to do it safely": if you use a theorem prover like Coq then you can formally verify any* code as correct, not just memory safe but truly bug free. See seL4. You'll have to write like 20 lines of proof code for every line of real code, and that code is difficult to write... but it's possible. On the other end of the scale, Rust doesn't have much annotation overhead, but if you truly want zero cost, the borrow checker has significant limitations - you can't have any cycles in your ownership graph, not even parent pointers. The alternative is to live with reference counting overhead, and I'm not sure how much benchmarking has been done of exactly how much overhead that is, but the community tends to value pragmatism over purity, so a lot of data structure libraries take the third option and use `unsafe` fairly liberally behind the scenes. (Which makes the parent's point somewhat inaccurate - Rust is not pure 100% memory safety; unfastening the seatbelt is possible. You just have to explicitly request it.) Of course, there is a huge gulf between those two paradigms. There are languages out there that could be said to live somewhere in the middle, like ATS, but they're not popular, and in general I think the spectrum is quite poorly explored. Certainly in theory there should be a fair amount of room to build from Rust's pragmatic approach and improve on it, by expanding what kinds of ownership models can be checked and/or reducing annotation overhead - but so far nobody has figured out what such an improvement could actually look like (except maybe this C++ thing, if it's not vaporware, heh), so it's up in the air how far this can be taken. I expect and hope Rust itself will continue to improve. * Technically not any, due to Gödel's incompleteness theorem, but certainly any code a human would write. (Anyone who cites either the incompleteness theorem or the halting problem as having practical relevance to basically anything in computing is mistaken.)