C has such types and can guarantee that there is no out-of-bounds access at run-time in the scenarios you describe: https://godbolt.org/z/f7Tz7EvfE This is one reason why I think that C - despite all the naysayers - is actually perfectly positioned to address bounds-safe programming.

Often in dependently-types languages one also tries to prove at compile-time that the dynamic index is inside the dynamic bound at run-time, but this depends.

▲ Sharlin 4 days ago | parent | next [-]

-fsanitize-bounds uses a runtime address sanitizer, surely? The program compiles fine. In a (strongly) dependently typed language, something like the following would refuse to typecheck:

  int foo(int i) {
      int bar[4] = { 1, 2, 3, 4 };
      return bar[i]
  }

The type checker would demand a proof that i is in bounds, for example

  int foo(int i) {
      int bar[4] = { 1, 2, 3, 4 };
      if i < 4
          return bar[i]
      else 
          return 0
  }

In languages with an Option type this could of course be written without dependent types in a way that's still correct by construction, for example Rust:

  fn foo(i: 32) -> i32 {
      let bar = [1, 2, 3, 4];
      bar.get(i)       // returns Option<i32>, not a raw i32
         .unwrap_or(0) // provide a default, now we always have an i32
  }

But ultimately, memory safety here is only guaranteed by the library, not by the type system.

▲

uecker 4 days ago | parent [-]

You seem to be repeating what I said except you mixup strong and static typing. In a statically dependent-typed language you might expect it this not to compile, but this also depends. Run-time checking is certainly something you can combine with strong dependent typing.

Implementing bounds checking that returns option types (which can also implement in C) is not exactly the same thing. But dependent typing can be more elegant - as it is here.

	▲	uecker 4 days ago \| parent [-]
		Update: For the interested, here are three ways to write this in C, the first using dependent type, the second using a span type, and the third using an option type. All three versions prevent out-of-bounds accesses: https://godbolt.org/z/nKTfhenoY

▲ turndown 4 days ago | parent | prev [-]

I thought that this was a GCC extension(you need to use #define n 10 instead of int n = 10). Is this not the case anymore?

	▲	uecker 4 days ago \| parent [-]
		This is in ISO C99. In C11 it was made an optional feature but in C23 we made the type part mandatory again.