Some code can be safe but is hard to reason about. The compiler tells you that. The solution is, unsurprisingly but perhaps disappointingly, to stop writing code like that.
Some code can be safe but is hard to reason about. The compiler tells you that. The solution is, unsurprisingly but perhaps disappointingly, to stop writing code like that.
This is a point I made back when I was doing verification. Yes, you can write code for which termination cannot be proven. If termination for your code is theoretically undecidable, it probably won't work right anyway. So don't go there.
Microsoft took a hard line on this with their Static Driver Verifier, a proof of memory correctness system for Windows kernel drivers. If your driver code is so hard to analyze that automatic path analysis can't verify memory correctness, it doesn't get signed to run in kernel space. Driver-caused Windows kernel crashes, formerly a huge problem, mostly went away.
But that is not easy, and much of that is due to the complexity of Rust and the way it handles memory safety. Which is where fighting the compiler comes in.
It is super hard if you actually know C/C++ or mastered a GC language. Rust won’t like some patterns at all and will fight you.
The point is, there are replacements for those patterns that are safer, about as performant and simultaneously easier to reason about by both you and the compiler. To stop fighting, you must switch to them. Old ways will not work. This is by design and a key point of Rust.
A single, concrete example: do not use references in object graphs. Use an array and indexes into it. If you have a dynamic structure with many additions and deletions, use generational indexing.