[amavect]

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.

[derdi]

What do you mean by notation like:

    Ensure y+x ≤ INT_MAX.

Is this supposed to be a precondition? Why would I want this precondition when using unsigned arithmetic?

[amavect]

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.

[kazinator]

In two's complement, calculating the overflow for addition is nearly exactly as complex as calculating carry for unsigned arithmetic.

Various versions of the Motorola 68000 programmer's manuals have a table which succinctly shows the Boolean formulas for calculating the flags for various operations.

In the following document it is Table 3-18. Integer Unit Condition Code Computations:

https://www.nxp.com/docs/en/reference-manual/M68000PRM.pdf

The ADD operation is in the second row of the table. See how in the right column, the calculation of C (carry out of highest bit) and V (overflow) have about the same complexity. V has only two "not" inversions compared to C's three, but otherwise both have six operands reduced via five "and" or "or" operations. C is a sum of two three-term products, V is a sum of three two-term products.

These calculations assume that we perform the addition as unsigned, and so we then have access to all three operands: the S, D, and R (source, destination and result). (That terminology is specific to the MC68K whose instruction set doesn't support the result going to a third operand which is not one of the two input operands.)

All the difficulties come from the higher level language semantics that don't provide a way to safely perform an overflowing operation and then detect overflow from a calculation applied to the two inputs and result.

I.e. some assembly-language-like "higher level" languages make things worse than assembly language, for the sake of abstraction and portability.

[amavect]

Cool!! I really like how the overflow condition reads. "When the source and destination have the same sign, but the result a different sign, then signed addition overflows."

x86 has SETC/SETNC and SETO/SETNO to pull the carry/overflow bits out of the status register.

  u+: ADD then SETNC
  u-: CMP then SETNC
  s+: ADD then SETNO
  s-: CMP then SETNO

C23 adds checked arithmetic, and gcc implements them as built-in, generating SETO/SETNO. I can't find a way to generate SETNO otherwise. https://godbolt.org/z/4EjecdW1d

  #include <stdint.h>
  #include <stdckdint.h>

  int add_u(unsigned x, unsigned y){
    return x <= ~y;
  }
  int sub_u(unsigned x, unsigned y) {
    return x <= y;
  }
  int add_u2(unsigned x, unsigned y){
    return !ckd_add(&x, x, y);
  }
  int sub_u2(unsigned x, unsigned y) {
    return !ckd_sub(&x, x, y);
  }
  int add_s(int x, int y){
    return !ckd_add(&x, x, y);
  }
  int sub_s(int x, int y) {
    return !ckd_sub(&x, x, y);
  }

Now, I the difficulty you talk about goes deeper than high level language semantics. Math and predicate logic can't easily talk about a carry flag or an overflow flag. Math equivocates unsigned comparisons with signed comparisons: unsigned < means carry flag, signed < means sign flag != overflow flag. Thus, by coincidence, unsigned < can talk about carry, but < cannot talk about only overflow (without the sign flag). Furthermore, a theorem-proving language wants to prove that overflow cannot happen before attempting to calculate it.

So, despite you clearly showing that carry and overflow have the same calculation cost, I don't know how to represent those predicates in a usual math language with equal symbol length or complexity.

[kazinator]

The important thing isn't the flag (piece of CPU state) but the function which calculates it from the two inputs and result. That is a pure Boolean function: do these three values indicate signed overflow or unsigned carry?

  int a = b + c; // safe version, like ADD on Motorola 68K.

  if (add_overflow_int(a, b, c)) ... macro/function determines overflow

The compiler could optimize that into accessing a flag, if the three inputs were just involved in an addition. In the general case, it has to emit the logic to test the bits of a, b, c.