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() t

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