On Mon, 10 Dec 2018, 09:30 Gershom B <gersh...@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. :)
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
