The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Andrew Pennebaker wrote:
> Adam, would Coq-based solutions be .vo files for obfuscation? <- That 
> can't be right; a secret proof is no proof.

No, .vo files contain proof terms, rather than proof scripts, which are 
more efficient to check, at no loss of trustworthiness.

> Aye, Haskell and Coq don't completely overlap, since Coq is 
> implemented in OCaml. But QuickCheck isn't only in Haskell; there's 
> already a port <https://github.com/camlunity/ocaml-quickcheck> for OCaml.

The problem of translating OCaml into Coq isn't obviously easier than 
translating Haskell into Coq.