User loginNavigation |
An experiment: Refined types - a better type system for more secure softwareHi, 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. By Tom Primožič at 2014-05-29 11:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 3940 reads
|
Browse archives
Active forum topics |
Recent comments
23 weeks 1 day ago
23 weeks 2 days ago
23 weeks 2 days ago
45 weeks 3 days ago
49 weeks 5 days ago
51 weeks 2 days ago
51 weeks 2 days ago
1 year 1 week ago
1 year 6 weeks ago
1 year 6 weeks ago