Hacker News

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:

  Ensure y+x ≤ INT_MAX.
  If x ≤ UINT_MAX-y, then x+y evaluates correctly:
  ∀x∀y(x ≤ UINT_MAX-y → ∃z(z = y+x))

  Ensure y-x ≤ INT_MAX.
  If x≤y, then y-x evaluates correctly:
  ∀x∀y(x≤y → ∃z(z = y-x))

The safety conditions for signed arithmetic:

  Ensure INT_MIN ≤ y+x and y+x ≤ INT_MAX.
  To avoid overflow or underflow, first compare x to 0.
  In the case x≤0, INT_MIN-x cannot underflow, and y+x cannot overflow. If y compares greater than INT_MIN-x, then y+x evaluates correctly.
  In the case 0≤x, then INT_MAX-x cannot overflow, and y+x cannot underflow. And if y compares less than INT_MAX-x, then y+x evaluates correctly.
  ∀x∀y((x≤0 ∧ INT_MIN-x≤y)∨(0≤x ∧ y≤INT_MAX-x) → ∃z(z = y-x))

  Ensure INT_MIN ≤ y-x and y-x ≤ INT_MAX.
  To avoid overflow or underflow, first compare x to 0.
  In the case 0≤x, INT_MIN+x cannot underflow, and y-x cannot overflow. If y compares greater than INT_MIN+x, then y-x evaluates correctly.
  In the case x≤0, INT_MAX+x cannot overflow, and y-x cannot underflow. If y compares less than INT_MAX+x, then y-x evaluates correctly.
  ∀x∀y((0≤x ∧ INT_MIN-x≤y)∨(x≤0 ∧ y≤INT_MAX+x) → ∃z(z = y-x))

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.

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.