<div dir="auto"><div><div class="gmail_quote"><div dir="ltr">On Mon, 10 Dec 2018, 09:30 Gershom B <<a href="mailto:gershomb@gmail.com">gershomb@gmail.com</a> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The other approach, which has been quite successful, by the penn team,<br>
is using hs-to-coq to extract coq from haskell and _then_ verify:<br>
<a href="https://github.com/antalsz/hs-to-coq" rel="noreferrer noreferrer" target="_blank">https://github.com/antalsz/hs-to-coq</a></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Thank you! Someone else proposed that off list yesterday too. If we get our layering right, that could definitely be a viable alternative!</div><div dir="auto"><br></div><div dir="auto">I will do some more research. I generally think that <a href="https://deepspec.org/">https://deepspec.org/</a> is an awesome idea. :) </div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto"></div></div>