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`.
> 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.
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`.