Mojo’s model looks interesting here. No GC and no ref counts, something akin to a reference count mechanism at compile time. Not sure how it works exactly and the documentation (as is the whole project) very alpha.
Is it impossible to prove memory safety in the general case due to the halting problem?
https://www.microsoft.com/en-us/research/publication/perceus...
It's interesting how much there still is to discover in this space, despite decades of research.