logoalt Hacker News

uecker • last Sunday at 5:26 PM • 2 replies • view on HN

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.

Replies

Sharlin • last Sunday at 7:46 PM

-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.
➕ show 1 reply
turndown • last Sunday at 5:42 PM

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?

➕ show 1 reply