4 ms·

For embedded code that must never fail. I don’t want array indexing, I can just use „get“

by selfmodruntime 2y ago

bestouff 2y ago
I would allow array indexing if the compiler can prove the bounds have been properly checked before use.
- SkiFire13 2y ago
  This is not that simple at all. For starters, what is a bound check? There's no such concept at the type level that the compiler can check. You'll need to add one such concept that propagates through functions, increasing the complexity of function signatures. And this still won't solve the problem of when you as a programmer know that something is definitely inbound but you can't express the proof in the language. Ultimately this means using `panic` (but you don't want to), dummy default values (but this is just `null` all over again!), adding dependent types (which AFAIK nobody has managed to do in a low level language, and even if it was possible it would add a lot of complexity) or just give up and accept your program cannot be accepted.
duped 2y ago
get() returns Option<T> which you need to match against, and if it's None then you may have no choice but to mark it unreachable!() which will panic in debug compiles. Or you can use get_unchecked which is unsafe and avoids the bounds check. If you pass the bounds check up higher then you have no risk of panic. My point is that forbidding code from panicking isn't that useful - you still need to audit the code to make sure it's correct.
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?).

For embedded code that must never fail. I don’t want array indexing, I can just use „get“

bestouff 2y ago

I would allow array indexing if the compiler can prove the bounds have been properly checked before use.

SkiFire13 2y ago
This is not that simple at all. For starters, what is a bound check? There's no such concept at the type level that the compiler can check. You'll need to add one such concept that propagates through functions, increasing the complexity of function signatures. And this still won't solve the problem of when you as a programmer know that something is definitely inbound but you can't express the proof in the language. Ultimately this means using `panic` (but you don't want to), dummy default values (but this is just `null` all over again!), adding dependent types (which AFAIK nobody has managed to do in a low level language, and even if it was possible it would add a lot of complexity) or just give up and accept your program cannot be accepted.

duped 2y ago

get() returns Option<T> which you need to match against, and if it's None then you may have no choice but to mark it unreachable!() which will panic in debug compiles. Or you can use get_unchecked which is unsafe and avoids the bounds check. If you pass the bounds check up higher then you have no risk of panic. My point is that forbidding code from panicking isn't that useful - you still need to audit the code to make sure it's correct.

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