> If you come up with a language design that is guaranteed to be memory-safe, eliminates array bound checks in most realistic use cases, and can be used by regular programmers, you will be hailed as a hero. I'm not exaggerating at all.
I'm just guessing, but wouldn't most uses of arrays be in traversing the whole array, ie mapping over the array, folding it etc.? I have seen a ton more
> for i = 0 to a.length -1
then I have seen something like indexing a sorted array like in a binary search. So if these operations are abstracted to functions that don't use array indexing directly, then they could perhaps be proven once in some library. And such a proof seems very straightforward (conceptually, perhaps not realistically) - just prove that your for loop exits when the index i gets incremented to out of bounds of the array.
I think Rust's iterators use no bounds-checked indexing underneath, at least for simple things like mapping over an array. They probably haven't proved that the indexing won't go out of bounds, though, probably just vetted and tested it a lot.
Yeah, Rust's iterators are a good example, and they indeed solve this specific use case.
(For those who don't know, an iterator in Rust has a function next() that returns an Option<A>. That allows you to do array bound checking and loop termination checking with a single operation, like when iterating over a linked list.)
Also I've seen a promising paper by Corneliu Popeea: http://gallium.inria.fr/~naxu/research/abce.pdf . It says it works on unmodified C code, doesn't require annotations, and successfully removes all checks in quicksort (!) Kinda sounds too good to be true though, I wonder what's the catch.
I'm just guessing, but wouldn't most uses of arrays be in traversing the whole array, ie mapping over the array, folding it etc.? I have seen a ton more
> for i = 0 to a.length -1
then I have seen something like indexing a sorted array like in a binary search. So if these operations are abstracted to functions that don't use array indexing directly, then they could perhaps be proven once in some library. And such a proof seems very straightforward (conceptually, perhaps not realistically) - just prove that your for loop exits when the index i gets incremented to out of bounds of the array.
I think Rust's iterators use no bounds-checked indexing underneath, at least for simple things like mapping over an array. They probably haven't proved that the indexing won't go out of bounds, though, probably just vetted and tested it a lot.