I’m afraid that what you’re proposing is either impossible or not too useful, depending on the scope you’re imagining. Ordinarily you wouldn’t ever be re-implementing addition on machine integers, so special analysis from the compiler on cases that don’t get far beyond your example might be fairly useless to people building real-world Rust applications. If you think of a larger scope on the other hand, then you must be careful not to over-estimate the “intelligence” of a computer, or a compiler in particular.
What I can tell from your (by the way a bit too short) “proposal” is that you’re asking about a compiler checking properties/correctness of a program. When we’re talking about arbitrarily complex properties we’re quickly hitting even the theoretical boundaries of what computers can automatically proof.
Also you’re suggesting for the compiler to look into comments and names of identifiers. It almost sounds like you would expect the compiler to understand the English language, or somehow guess what the developer had in mind, two things that computers in general are, as of now, not really capable of doing at-all.
Something that is possible however is for computers to check correctness properties of programs that are formally specified by the programmer in some way and where potentially even some form of proof is given. In the context of Rust this is what the type system is for. You could interpret the situations where you’re fighting with the borrow checker as refactoring your program to (implicitly) give some proof that you’re doing things correctly around Rust’s ownership semantics.
Type systems can go way further though, I’m afraid this is not something that will come to Rust anytime soon, but if you search the internet for “automatic theorem proving” of “proof assistants” or in particular “dependent types” you might find some material on this kind of topic in the meantime.