www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Refinement types in OCaML

https://github.com/tomprimozic/type-systems/tree/master/refined_types

The implementation of a refined type-checker is actually very 
straightforward and turned out to be much simpler than I 
expected. Essentially, program expressions and contracts on 
function parameters and return types are converted into a series 
of mathematical formulas and logical statements, the validity of 
which is then assessed using an external automated theorem 
prover Z3.<

It seems possible to integrate Z3 with D contract programming. Bye, bearophile
May 31 2014