> This is a very common misconception that stemmed from a recent conversation with one of my non-Rust engineer colleagues. For him, it was inconceivable that a Rust program would panic because of an out-of-bounds runtime memory fail.

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.

Proving that array-out-of-bounds never happens is just a special case of proving that an assertion error never happens, which is intractable in the most general case.

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