seems to be gaining some traction as a GHC plugin
https://ucsd-progsys.github.io/liquidhaskell-blog/2020/08/20/lh-as-a-ghc-plugin.lhs/
but hs-to-coq is easier to use. https://nikivazou.github.io/static/Haskell17/a-tale.pdf
It might be a way of slowly luring haskell programmers to Coq...
I think they also have an integration problem, ideally they would merge hs-to-coq with https://github.com/jwiegley/coq-haskell
They agree :-)
https://github.com/antalsz/hs-to-coq/issues/122
Last updated: Oct 13 2024 at 01:02 UTC