> even if they're not literally written in the code

Yeah, that was my point. While you would still need to follow Rust's lifetime rules, they wouldn't need to be explicitly expressed in the code. This comes from a discussion I was having with some Rust people about extracting Rust's static verifier/"borrow checker" so that it could be applied to C/C++ code (or at least SaferCPlusPlus code). Some of them seemed to claim that this was not really possible do to the lack of lifetimes annotation in C/C++. But if all that's required is implicit lifetime specification rather than explicit lifetime annotation, then I don't see why the static verifier couldn't be applied to C/C++ code. The author of the OP suggested (somewhere in his blog) that you could effectively use Rust's static verifier on C code by using his tool to translate the code into Rust and see if it compiles. Which would be essentially equivalent to repurposing Rust's static verifier to work on C code. So I was just trying to express my agreement with the plausibility of this notion, where others might be skeptical.

> I would expect a lot of such code is only dynamically correct.

Yes, my view is that it would be better if the "brains" of the static verifier were instead in the optimizer. That is, rather than refusing to compile code that cannot be statically verified to be safe, you could require that code have run-time checks to ensure memory safety (either by using a library like SaferCPlusPlus, or by having the compiler inject them automatically). If the optimizer can recognize that the code is intrinsically safe (in the same way the borrow checker does), then it could simply strip out the unnecessary run-time checks.

If the optimizer reported which run-time checks it was not able to discard, then the functionality of the optimizer would be a superset of the functionality of the static verifier. That is, if you self-impose the requirement that all run-time checks be optimized out, then you'd have the exact same functionality as the static verifier.

The benefit to this approach is i) sometimes you don't care if the code is statically or dynamically correct (or you know that it's correct and you don't care whether the compiler recognizes it or not), and you don't want to bother having to contort your code to appease the borrow checker. But perhaps more importantly, ii) the "(hopefully optimized out) run-time checks" approach scales better to higher (application) level notions of "correctness", not just memory safety. Right?

And perhaps less importantly, iii) as the compiler (optimizer) gets smarter (i.e. is able to discard more run-time checks), existing code benefits (by getting slightly faster).

> what do you mean by rebindable and non-rebindable references?

I mean references that can be reassigned to point to another variable. I thought the term "mutable reference" might be unclear as to whether reference itself was reassignable or that it facilitated mutation of the thing being referenced. I got the "bind" term from some Rust document that was trying to clarify this "mutable reference" ambiguity. The term used throughout the SaferCPlusPlus documentation is "retargetable". Would that be more clear? I'm open to suggestions.

> The restriction on multiple aliasing for mutable references is not just to avoid objects being deallocated, it avoids things like iterator invalidation and concurrency problems like data races.

Of course you're right, but I don't think it affects the clarity of the point being made. I'm open to any suggestions for a better rephrasing.