[cloud-haskell-developers] Does anyone have much experience generating Haskell from Coq?

[Tim Watson]

On Mon, 10 Dec 2018, 09:30 Gershom B <gershomb at gmail.com wrote:

> The other approach, which has been quite successful, by the penn team,
> is using hs-to-coq to extract coq from haskell and _then_ verify:
> https://github.com/antalsz/hs-to-coq


Thank you! Someone else proposed that off list yesterday too. If we get our
layering right, that could definitely be a viable alternative!

I will do some more research. I generally think that https://deepspec.org/
is an awesome idea. :)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181210/95a1047b/attachment.html>