I feel like this all motivates for a very expressive type system for integers. Add different types for wraparound, saturation, trapping, and undefined. Probably require theorem proving in the language to provably never overflow for undefined overflow integers.
>knowing that (A + (B + C)) can't overflow doesn't mean that ((A + B) + C) can't overflow
Here, the associative property works for unsigned integers, but those don't get the optimizations for assuming overflow can't happen, which feels very disappointing. Again, adding more types would make this an option.
I am not sure more types are the solution. I like types, but I do not like complicated things.
The practical solution is simply -fsanitize=signed-integer-overflow. If you need complete assurance that there can not be a trap at run-time, in the rare case where I wanted this, just looking at the optimized code and making sure the traps have been optimized out was surprisingly effective.
>knowing that (A + (B + C)) can't overflow doesn't mean that ((A + B) + C) can't overflow
Here, the associative property works for unsigned integers, but those don't get the optimizations for assuming overflow can't happen, which feels very disappointing. Again, adding more types would make this an option.