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

On Mon, 10 Dec 2018, 09:30 Gershom B <gershomb@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. :)