Eliminating array bounds check

[oleg@pobox.com]

On Aug 31, John Skaller wrote:
> Typing is always an abbreviation (abstraction) and sometimes
> stronger or weaker than desired: for example array bounds
> checks at run time, because the type system doesn't cope
> with array sizes as part of the type.

Although that is true that making the type system track the size of a
(dynamically allocated) array is too much of a hassle, array bounds
checks at run-time can be entirely and safely avoided, in OCaml as it
is.

For example:
 http://pobox.com/~oleg/ftp/ML/eliminating-array-bound-check-literally.ml

shows how to implement the bsearch (the standard Dependent ML example
from the famous Xi and Pfenning's PLDI98 paper) in the current
OCaml. The above code has exactly the same number of checks as the DML
code; there are no array bound checks -- and yet the code has the same
static assurances of the absence of out-of-bounds array access
errors. The code (given at the end of that file) even looks quite like
the original DML code (quoted at the beginning of that file), only
without any type annotations.

A more interesting example is the textbook KMP string search, which
uses mutable arrays, general recursion, and creative index expressions
(with mutable arrays storing array indices).

  http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html

(well, the referenced code is actually in Haskell, but it is easy to
re-write it in OCaml; I can do that if called to). 

The above page points to the PLPV talk that contains formalization and
the proof method (as well some proofs in Twelf). Briefly, we rely on
the type system to propagate assurances made in a small `security
kernel' through the rest of the code. The security kernel does have to
be verified. Our examples show that the kernel is far simpler than the
rest of the code: the KMP kernel, for example, is made of
non-recursive functions performing additions and subtraction of
integers.