In a language that has arbitrary precision integers, you'd pretty much never want them unsigned, or even to have signed and unsigned flavors.
Whether unsigned or signed is better is a matter that is a combination of personal opinion and the quirks of a given systems programming fixed integer language.
The trade-off reasoning would be different, for instance, in a language that requires implementations to provide two's complement signed integers, with wraparound semantics. Or, say, no wraparound semantics but a robust overflow detection system coupled to exception handling.
There are other matters beside overflow, like conversions. In C, mixtures of signed and unsigned bring in some implementation-defined conversion rules, which nudges the argument toward "all unsigned" or "all signed" for the sake of avoiding mixtures.
I like to trot out the following argument.
Suppose a, b and c are small integers close enough to zero that any additive/subtractive combination of them is free of overflow.
If they are signed, then we can make inequality derivations like
a + b < c
b < c - a // subtract a from both sides; "bring to other side"
If they are unsigned, then we cannot do this. That is a barrier to refactoring code with arithmetic conditionals and just reasoning about it.
I believe the main issue lies in most programming languages lacking theorem proving capabilities to prove the safety of integer operations.
The safety conditions for unsigned arithmetic:
The safety conditions for signed arithmetic: The programmers that prefer unsigned arithmetic intuitively feel the greater simplicity compared to signed integers, but without any theorem proving, I agree that your assumption of small integers strongly supports signed integers.What do you mean by notation like:
Is this supposed to be a precondition? Why would I want this precondition when using unsigned arithmetic?I included that to try to explain the symbol soup that correctly encodes the preconditions (the ∀ lines). I intended that to mean "I need to make sure that y+x doesn't overflow", even that unsigned arithmetic cannot express that precondition in that way, as you point out. From there, derive y ≤ INT_MAX-x as the actual precondition for unsigned addition. I forgot that "ensure" actually means something in some programming languages, sorry for the confusion.
More simply put, unsigned addition needs to check that y+x doesn't overflow, while signed addition needs to check that y+x doesn't overflow and doesn't underflow. So, unsigned arithmetic has a simpler precondition that would win a technical debate on whether to use signed or unsigned arithmetic, but since most programming languages lack theorem proving, signed arithmetic wins on the small integer assumption.
[dead]