Comment by cousin_it | Hacker News Reader

Comment by cousin_it | Hacker News Reader

Parent Full thread

Any such system would need a theorem prover that's powerful and easy to use, and such a prover doesn't exist. For example, to implement an algorithm that involves arrays and indices, you'd need to supply machine-checkable proofs that all indices involved in the algorithm are valid for their respective arrays. That's really difficult, e.g. you can try to come up with some static reasoning scheme that would work on this algorithm:

http://en.wikipedia.org/wiki/Knuth%E2%80%93Morris%E2%80%93Pr...

The original paper on this topic is Hongwei Xi's "Eliminating array bound checking through dependent types", http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf . You will note that he failed to remove all bound checks in the algorithm, even though he started out with a good language (ML), added many manual annotations, and used a sophisticated method of automatically proving theorems. Also, his method and most subsequent methods will fail on any problem that involves multiplication of integers to get array indices, e.g. addressing a rectangular array as a[i*n+j], because integer arithmetic with multiplication is undecidable and even simple instances make the computer cry.

This is a hard research problem. 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.

Elaborating on my previous reply.

The way I wish things worked:

Programmers code with three types of constraints: soft cast, hard cast, and unsafe cast. Soft cast is a runtime assertion that the constraint isn't violated, hard cast is a "do not compile unless you can prove that this constraint isn't violated" and unsafe cast is a "check at compile time to make sure you cannot provide a counterexample, but do not include a runtime check". Hard cast will be rarely used, for obvious reasons.

Compiler propagates known values / constraints forwards as much as possible, and propagates constraints backwards as much as possible. Note that this generally already happens as part of compiler optimizations. If at any point any value violates a constraint, error out and provide a "constraint trace" of what caused the violation.

After this step, the compiler looks at all unknown-at-compile time variables and randomly (or rather, pseudo-randomly, maybe seeded with the md6 of the file or something to be deterministic) generates and tests values (along with some common values - note that this could be integrated with a test framework built into the language!), ensuring that no constraints are violated. (There are a bunch of optimizations here that I'm not going to mention.) If any constraints are, error out with the variables required to violate the constraint and the values assigned to them.

This is too much machinery to build into a general-purpose compiler today, but there are static analysis tools (see Frama-C and the like) that will analyze your program text (optionally with annotations like you've mentioned) and figure out constraint violations.

Well, the thing is, anything would be better than what we have currently.

I know that in general the problem is undecidable. But we don't need to solve the entire problem to solve a large chunk of practical cases.

Even a simple runtime cast (with check) / asserting cast (a cast with an assertion that would be triggered at compile time if the compiler can find a valid counterexample, otherwise unchecked) combination would be miles above what we have now in most strongly typed languages.

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

Not only quicksort, but recursive quicksort.

That indeed looks promising!

Reply on news.ycombinator.com