Dependent typing and Refinement Typing for D

bpr brogoff at gmail.com
Sun Dec 22 00:52:56 UTC 2019


On Friday, 20 December 2019 at 22:06:03 UTC, sighoya wrote:
.
.
.

I realize this is a D forum, but it seems highly unlikely to me 
that you'll be able to get anywhere trying to add this stuff to 
D. If you don't know, there is a research language called F* or 
Fstar that integrates dependent types, refinement types, the Z3 
prover, and more. It has a low level subset called Low* and a 
backend which can emit verified C, and has been used to implement 
verified cryptographic libraries.


More information about the Digitalmars-d mailing list