story
While it'd be nice to have a formal proof that every single `a+b`, `a-b`, `a*b` in every codebase doesn't overflow, I'm sure you understand that that is rather impractical. (and really, it'd be nice! I've thought about having some compile-time-bounded-size integers where each addition increases the size, but multiplication is much less suitable for that, and it also means you can't have a loop adding to an accumulator. It's a rather non-trivial problem really - you might think that it'd be fine to have a loop over a list of objects and sum their sizes, but that can relatively easily overflow if the list references the same massive object many times, so can't even really abstract that)