wilcoxjay

3 ms·

1. 1.▲
   Hs-to-coq: Haskell to Coq converter(github.com)

   2 points by wilcoxjay 9y ago|0 comments
2. 2.▲
   by wilcoxjay 11y ago

   This is a great question that permeates all verification work. In the lingo, we call the set of assumptions a proof makes the "trusted computing base" (see https://en.wikipedia.org/wiki/Trusted_computing_base
3. 3.▲
   by wilcoxjay 11y ago

   Hey, I'm James Wilcox, another member of the Verdi team. This is a good question. More broadly, what do you have to trust in order to believe our claims? In addition to all the usual things (like the soundness of Coq's logic and t