HACL*, a formally verified cryptographic library written in F*

https://github.com/hacl-star/hacl-star

#FStar #FStarLang #Cryptography #FormalVerification

One thing I'm coming to appreciate about #LiquidHaskell is that lazy execution simplifies the handling of code whose only purpose is to generate a needed type (like a lemma.) In #FStarLang these are explicitly "ghost" functions which don't appear in the generated code. In Haskell, if you don't use the value, it just doesn't get executed!