The only way this can work in practice is restricting the memory patterns that the developer can use, which is what we see in Rust.
Is it impossible to prove memory safety in the general case due to the halting problem?
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.