An experiment: Refined types - a better type system for more secure software
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
Read more about it (and see the code) here! Any comments are welcome.
Active forum topics
New forum topics