Yeah, I'm wondering how that would look at the assembly level. In the "x + y - z" example we get an overflow from the "x + y" and an underflow when we add z. So

Yeah, I'm wondering how that would look at the assembly level. In the "x + y - z" example we get an overflow from the "x + y" and an underflow when we add z. So you'd have to check if the number of overflows and the number of underflows are equal, and the assembly would probably be really slow. You'd want some kind of bounds check optimization to try and remove as many of those checks as you can. Fortunately, I don't think these issues will appear too often (at least they haven't in my experience), and you can probably get away with just adding unit tests. To be completely thorough you should probably use some sort of formal modeling and proof system, which I would like to see someone try and develop for Rust.