-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