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?
Page 15 in the paper does a comparison: https://hal.inria.fr/hal-02422273/document
It's your lucky day :-)
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 :)
If you are interested in investing some time in FreeSpec, feel free to ping me! I would love to help.
@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
@Karl Palmskog It definitely is in my todolist! and I hope to be able to do so in September
thanks for the suggestion
@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: Sep 30 2023 at 16:01 UTC