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. :)