I think you'll find that if you encode these guarantees into the language level itself, that won't allow the programmers involved to stop thinking about the math. Either your language won't allow them to express the first thing they want to express, and they'll have to figure out how to do it with the proper mathematical primitives (and they'll complain up a storm about how useless your language is on the forums), or it will allow them to express it but yield a compile-time "Operation violates monotonicity constraints at line 88..." and they're going to have to understand that fairly deeply, or also end up dropping your language when they can't scale up their program because the "blunder around adding and removing sigils and annotations and sprinkling in 'unsafe' until the compiler shuts up" just doesn't scale very far beyond "complete the school assignment due tomorrow".

Look at Rust. Putting memory management concerns in the language front and center doesn't relieve you from having to thinking about them. It means you have to think even more deeply about them. Fortunately, this is the correct thing to do, and it get easier with practice, and is also easier to learn when it's so strongly highlighted instead of implied and buried. But if anything, it forces a more mathematical way of thinking on to you. (Reasoning about scopes is the foundation of the mathematical discipline of structured programming.)