Ada solved these problems in 1983.

More recently, you can use Frama-C to constrain allowable sequences of 0's and 1's for C types and formally verify correctness.

In Ada since 1983 you can, e.g, declare your own 8 bit signed symmetric type without the wart -128 like so:

  type Sym_8 is new Integer range -127 .. 127;

Then this fails at compile time:

  My_Signed_Byte : Sym_8 := -128;
  

SPARK can prove all execution paths through your program are free of such constraint violations. This means safe SPARK code can disable runtime checks and run faster than the safest Rust/Zig dev settings, which insert runtime checks for over/under flow.

In Frama-C, say you want a function that returns an absolute value. This function will fail to verify:

  /*@ ensures (x >= 0 ==> \result == x) &&
              (x < 0 ==> \result == -x);
      assigns \nothing;  */
  int abs (int x) {
      if (x >=0)
          return x;
      return -x;
  }

It fails to verify because you might have x==INT_MIN. So this will verify:

  #include <limits.h>
  /*@ requires x > INT_MIN;
      ensures (x >= 0 ==> \result == x) &&
              (x < 0 ==> \result == -x);
      assigns \nothing;  */
  int abs (int x) {
      if (x >=0)
          return x;
      return -x;
  }