I'd add that Frama-C does also this kind of proof and IIRC Eve (Eiffel Verification Environment ?) too, though I find the SPARK workflow far easier and advanced (but we use it more so... I'm biased).
It's a type constraint on the index. In most programming languages we're used to the index value is some machine type, like a 32-bit unsigned integer, but that's arbitrary, the language can say OK, this is an index into an array of sixteen things, so, the index must be between 0 and 15 inclusive.
Now, depending on the software you might just have to write bounds checks yourself to satisfy this constraint, so you just made more work for yourself, but if your software actually deals in types that can and perhaps should be constrained properly elsewhere this approach means you get a compiler error not a runtime failure.
Suppose we've got code that does foo[k] where foo is an array of eight things and k is an unsigned variable with the bottom four bits of a value from an image file that's supposed to be the CGA medium resolution colour palette ID (0, 1, or 2). Alas the file might be corrupt or malicious and those bottom bits could be, for example 10.
In C and C++ foo[k] compiles, and when the corrupt file is used there is Undefined Behaviour
In Rust foo[k] compiles, and when the corrupt file is used the program panics on this line
In WUFFS foo[k] doesn't compile, variable k is the wrong type for indexing foo.
https://github.com/google/wuffs/blob/main/doc/wuffs-the-lang...
Now, WUFFS is not a general purpose programming language. You should not write an operating system, a web server, a compiler in WUFFS. But, you should write your thumbnail making routine, your PDF validation code, your audio compressor in WUFFS, because in choosing not to be a general purpose language WUFFS is freed to simply always be safe. That WUFFS thumbnail code might make the RCE attempt from Leet Hacker into a blue rectangle, or crop all the executives photos to just their nose, but it simply cannot accidentally create a reverse shell, or spew passwords into the thumbnails, or a billion other things which Rust would make difficult to do by mistake but never impossible.
> It's a type constraint on the index
Consider a program in which the index type is provided by some user input -- how could this ever be proven to never go out of bounds?
You can move the problem elsewhere (and indeed often should!), but eventually it becomes a condition check and error handling behavior appropriate to the scenario. The default error handling behavior is to halt the program.
Claim: Rust enables you to eliminate many classes of bugs at compile-time. (https://www.rust-lang.org, "Why Rust?", "Reliability")
Reality: Rust enables you to eliminate an extremely limited class of bugs at compile time, and also inserts if statements into your program to detect some other classes of bugs at runtime and crash cleanly.
I've done this in Ada/SPARK.
My simple_regex implementation of Rob Pike's algorithm [1] based on this blog post [2], is proved not to crash on overflow or bounds checks.
If I wanted to do something to validate an entire program subset similarly, I'd make a type with the bounds I needed that gets fed into that algorithm which is proved for those ranges. This isolates the proved code from user input, but the newtype with range ensures those checks are done prior to being fed into the algorithm. You can't "prove" user input, there has to be validation, but you can force that validation prior to entering the proofed code.
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)
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.
I feel like this is just a misunderstanding (probably from a somewhat junior engineer, or at least an engineer unfamiliar with low-level programming) between segfault and panic.
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?
Rust won't segfault here like some naive C will, but it will panic, because you hit the assertion that the index is less than the length of the array.
Formal verification to prove that a program will never panic is a very neat field unto itself. There is some work in this space in Rust, but it's bolted on top, not built into the language (this is the case for most formal verification of most non-research languages).