3 ms·
If you want to prove that an array is never indexed out of bounds in some procedure for an embedded program, you can use Ada with SPARK or use Frama-C to prove
by trealira 2y ago
If you want to prove that an array is never indexed out of bounds in some procedure for an embedded program, you can use Ada with SPARK or use Frama-C to prove it. As far as I know, Rust has no equivalent.
Otherwise, like duped said, using get will return an Option<T>, and so you'd either have to use unreachable!() and panic anyway, or you'd have to propagate the error up the call stack and let it affect all the types of those functions (at which point, what is the caller supposed to do about it?).