Lambda the Ultimate

Hi, fellow language enthusiasts!

I recently finished an experimental, fairly simple, OCaml implementation of refined types. Refined types support logical predicates in function parameters and return types, for example:

/ : (int, i : int if i != 0) -> int

random1toN : (N : int if N >= 1) -> (i : int if 1 <= i and i <= N)

length : forall[t] (a : array[t]) -> (l : int if l >= 0)

get : forall[t] (a : array[t], i : int if i >= 0 and i < length(a)) -> t

Refined types are checked by an external automatic theorem prover (Z3), and can prevent many common software errors, such as division by zero and out-of-bounds array access. Given correct refined types on functions alloc and memcpy, they could even be used to prevent Heartbleed bug!

Read more about it (and see the code) here! Any comments are welcome.