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`.
You can't, because indexing is required to return a reference. It's hard to get creative.
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.
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)