3 ms·

> Consider a program in which an array was accessed based on the index provided by some user input -- how could this ever be proven to never go out of bounds?

> Consider a program in which an array was accessed based on the index provided by some user input -- how could this ever be proven to never go out of bounds? In fairness, the approach to similar operations in Rust is usually by returning an Option or a Result, so it is arguably counterintuitive that a few specific operations like array indexing panic instead. (you can do Vec.get(), but normally the "safe" behavior is the default and the "unsafe" behavior is optional and more verbose, e.g unwrap)

gamegoblin 4y ago
IMO this kind of just moves the goalpost from "prove the program never panics" to "prove the program never hits the `None` or `Err` path" which is functionally identical in most use cases. Obviously I am not suggesting that people use `arr[i]` everywhere and try to catch the panic, this is an antipattern -- use `.get(i)` if you don't know the bounds. I'm just talking about for the purposes of program formal verification. Aside: I think the language design team making the most terse `arr[i]` code not need unwraps or anything was the right move. Doing `.get(i)?` or `.get(i).unwrap()` all over the place is too much visual clutter. If the user really wants, they can make a custom slice wrapper that implements the `Index` trait in a way that returns `Option`.
- duckerude 4y ago
  > If the user really wants, they can make a custom slice wrapper that implements the `Index` trait in a way that returns `Option`. You can't, because indexing is required to return a reference. It's hard to get creative.
- dllthomas 4y ago
  > IMO this kind of just moves the goalpost from "prove the program never panics" to "prove the program never hits the `None` or `Err` path" which is functionally identical in most use cases. If my goal is to show that a piece of code never panics, then it suffices to show that the None or Err path doesn't panic; I don't need to show that it's never hit.

gamegoblin 4y ago

IMO this kind of just moves the goalpost from "prove the program never panics" to "prove the program never hits the `None` or `Err` path" which is functionally identical in most use cases. Obviously I am not suggesting that people use `arr[i]` everywhere and try to catch the panic, this is an antipattern -- use `.get(i)` if you don't know the bounds. I'm just talking about for the purposes of program formal verification. Aside: I think the language design team making the most terse `arr[i]` code not need unwraps or anything was the right move. Doing `.get(i)?` or `.get(i).unwrap()` all over the place is too much visual clutter. If the user really wants, they can make a custom slice wrapper that implements the `Index` trait in a way that returns `Option`.

duckerude 4y ago
> If the user really wants, they can make a custom slice wrapper that implements the `Index` trait in a way that returns `Option`. You can't, because indexing is required to return a reference. It's hard to get creative.
dllthomas 4y ago
> IMO this kind of just moves the goalpost from "prove the program never panics" to "prove the program never hits the `None` or `Err` path" which is functionally identical in most use cases. If my goal is to show that a piece of code never panics, then it suffices to show that the None or Err path doesn't panic; I don't need to show that it's never hit.