Re. syntax. I don't understand, why can't they just make _Ptr an attribute like _Atomic, and provide a header <stdchecked.h>. That is,

  #include <stdchecked.h>

  void read_next(int *b, int idx, checked int *out) {
      int tmp = *(b+idx);
      *out = tmp;
  }