Refinement types in OCaML

[bearophile via Digitalmars-d]

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