Lee (Aug 26 2020 at 14:29): Lee (Aug 26 2020 at 14:29):New and excited about software verification, I've stumbled on Coq.io. Then shortly the author of Coq.io mentioned FreeSpec. From what I understand these two technologies solve the same problem. My question is, why would I use one over the other? From what I see, Coq.io is simpler conceptually and in implementation, whereas FreeSpec is modelled around a free monad and more theory heavy.
Is there some advantage to FreeSpec's more detailed implementation? Or is it all just a formality?
Karl Palmskog (Aug 26 2020 at 14:49):Page 15 in the paper does a comparison: https://hal.inria.fr/hal-02422273/document
Bas Spitters (Aug 26 2020 at 15:02):It's your lucky day :-)
https://github.com/coq-community/manifesto/issues/114
Lee (Aug 26 2020 at 15:45):Thank you very much. That page in the paper does a perfect job of explaining the state of things.
coqffi looks interesting, but this is not something I think I'd use. Thank you for sharing regardless :)
From what I understand FreeSpec seems more powerful at the cost of needing to learn more. Seems like a fair trade off :)
Thomas Letan (Aug 27 2020 at 22:02):If you are interested in investing some time in FreeSpec, feel free to ping me! I would love to help.
Karl Palmskog (Aug 27 2020 at 22:12):@Thomas Letan one thing that could help/encourage people to use FreeSpec would be to package it in the Coq opam repo, either as a development package, or via releases/tags in the released repo
Thomas Letan (Aug 27 2020 at 22:13):@Karl Palmskog It definitely is in my todolist! and I hope to be able to do so in September
Thomas Letan (Aug 27 2020 at 22:13):thanks for the suggestion
Lee (Sep 09 2020 at 01:03):@Thomas Letan absolutely! For now I'm still working my way through Logical Foundations. I'm not sure I'll go all the way through volume 2 before starting to play with FreeSpec.
Last updated: Oct 13 2024 at 01:02 UTC