Wuffs is a language by Google that allows safe parsing without runtime bound checks, by forcing the coder to prove an array access is within bounds before acessing.
Rust's runtime bound checker is enough for 99% of applications, but there's a niche for languages like Wuff which is when bound checks hurt performance for ultra critical fast parsing like a server parsing millions of images.
Couldn't Rust implement something like this? When disabling bound checking, instead of doing an unsafe operation, we should prove that we can disable it. Just as lifetimes prove to the compiler that it's safe to accept a reference for some period of time.
This would make Rust even safer as some people might try to do these performance critical things in unsafe code and mess things. Also, interfacing Wuffs with Rust is unsafe. Imagine if we had safe unbound-checked arrays in Rust (for these specific cases).
The way WUFFS accomplishes this is by being a very simple, non-general-purpose language. In general, it is quite difficult to prove things like this without an SMT solver like Z3, which is not something I think many people would be hot about adding to Rust. In general, the correct(tm) way to avoid bounds-checks in rust is to use iterators, which will be optimized down to a loop without bounds checks.
That said... once generics-dependent-const-eval-in-const-generics is sorted out, it would be very nice to have types like Bounded<u8, 1..=255> which can be used for safely indexing into arrays of known size, e.g.
See the indexing crate, which is a proof of concept that this can be done already in userland. I've an abandoned fork that tried cleaning stuff up and added support for indexing &str, but abandoned it because actually using it is harder than is worth for any of my applications, due to its generality.