Stream: Coq users

Topic: FreeSpec vs Coq.io ?


view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Aug 26 2020 at 14:49):

Page 15 in the paper does a comparison: https://hal.inria.fr/hal-02422273/document

view this post on Zulip Bas Spitters (Aug 26 2020 at 15:02):

It's your lucky day :-)
https://github.com/coq-community/manifesto/issues/114

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Thomas Letan (Aug 27 2020 at 22:13):

thanks for the suggestion

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC