Oh, not Rice's theorem again. That only applies to infinite systems. There are useful decidable properties for a reasonably large set of programs. Yes, they're "uninteresting" mathematically, but we're talking about memory safety here. If your program is anywhere near undecidable in that area, you're doing it wrong. Any time you're close to the edge on that, you can get decidability with a run-time check. The Microsoft Static Verifier people have been down that road with some success. I went there 40 years ago, with the Pascal-F Verifier.
The question I'm asking is, what do you really need to do that you can't do in safe code. On the memory safety front, for pure Rust (no calls to C), probably not all that much. Maybe only this:
- Syntax for talking about partially initialized arrays. For a collection, you have a variable that indicates how much of the array has been initialized, and you need a statement in the language that ties that variable to a partially initialized array. Then you can do simple inductive proofs to show that as you initialize another element and add 1 to the counter, the entire array is initialized. Non-consecutive initialization would require more complex proofs. Is there a real use case for that? One with major performance implications, where initializing the data to some null value would be too slow?
Un-initialized blocks of types such as raw bytes aren't a problem, because those types are "fully mapped" - all bit combinations are valid. Only types that are not fully mapped an initialization guarantee.
- Backlinks. Backlinks in doubly-linked lists and trees obey some simple invariants. You need syntax to say "this is a backlink". That implies an invariant that if A points to B, B must point back to A. Everything which updates A or B must preserve that invariant. The pointer from B back to A then no longer needs to have ownership of A. (It's a problem that Rust doesn't have "objects", because such invariants are usually required to be true when control is outside the object, but can be broken momentarily while control is inside it. The inside/outside distinction is important for this, and Rust is a bit soft on that. Spec# took inside/outside seriously, but viewed it dynamically, rather than being tied to static scope. Haven't looked at that in years.
What else do you really need? Remember that some knotty ownership problems can be resolved by allocating the objects in an array which owns them, and using array indices for relationships between the objects. It's not like you have to use pointers.
Concurrency is a related issue, but I've said enough for one night.