Achieving Safety Incrementally with Checked C

It is so hard that a large majority of system programming languages do it.

That Pascal example is getting tired by now. It only applies to the first edition of ISO Pascal (superceded by ISO Extended Pascal), and improved by any systems language that was born afterwards.

First of all, outside Bell Labs there were computers being programmed in high level languages since 1961, definitely much weaker computers than a PDP-11.

Secondly, ptr = &array[0] is something would happen at compile time.

Third, C authors seem to have a predisposition to ignore state of the art in existing languages.

OK, Here's a non-string function where the translator is trying to deal with C written like it's 1980:

    static unsigned countZeros(MSE_LH_ARRAY_ITERATOR_TYPE(const unsigned char) data,
        size_t size, size_t pos)
    {
      MSE_LH_ARRAY_ITERATOR_TYPE(const unsigned char)  start = data + pos;
      MSE_LH_ARRAY_ITERATOR_TYPE(const unsigned char)  end = start + 
          MAX_SUPPORTED_DEFLATE_LENGTH;
      if(end > data + size) end = data + size;
      data = start;
      while(data != end && *data == 0) ++data;
      /*subtracting two addresses returned as 32-bit number
          (max value is MAX_SUPPORTED_DEFLATE_LENGTH)*/
      return (unsigned)(data - start);
    }

What guarantees that the "while" loop will not run away and take "data" outside the array bounds?

I proposed a version of C with slices and references, where you could write that like this:

    static unsigned countZeros(const unsigned char &(data)[size],
        size_t size, size_t pos)
    {
      const unsigned char &(data1)[size-pos] = data[pos:size-pos]; // slice
      size_t cnt = 0;
      while (cnt < LENGTH(data1) && cnt < MAX_SUPPORTED_DEFLATE_LENGTH && data1[cnt] == 0) ++cnt;
      return(cnt);
    }

The "data" parameter has size info, so the language knows how big it is. The "work" variable is a slice of "data". This eliminates the need for pointer arithmetic. Much pointer arithmetic in C, especially where you have a pointer partway into an array, is an attempt to emulate a slice.

Automatically extracting slice usage from code with pointer arithmetic is a tough problem. But not impossible. When you see code constructing something like

    data = start;
    while(data != end && *data == 0) ++data;

you have to recognize that as subscripting.

    while(data != end && *data == 0) ++data;
    return (unsigned)(data - start);

should become first

    data = start;
    size_t dataix;
    while(&data[dataix] != end && data[dataix] == 0) ++dataix;
    return (unsigned)(&data[dataix] - start);

by substituting subscripting for pointer arithmetic.

Next, when you see an offset array being created, as in

    start = data + pos;

turn that into a slice:

    const unsigned char &(data1)[size-pos] = data[pos:size-pos]; // slice

The slice is the same pointer, but the there's now valid size information associated with it.

If you do transformations like that, you get a version of C where subscript checking is possible. You can then hoist or prove out many of the subscript checks. Here, the compiler would be expected to understand that if an array subscript is less than LENGTH of the array, it's safe. LENGTH here, as I wrote in my paper, refers to the length of the array as known to the compiler from the array declaration. Here, array lengths can be expressions evaluated at declaration time. That's how length info gets passed around.

    const unsigned char &(data)[size]

as a parameter means "this is an array of size "size". "size" comes in via another parameter. The function can assume "size" is valid, and all callers must check that, either at compile time or run time.

If you can't write an expression for the size of something, you have a big problem with your program.