The Coq Platform developers might enjoy reading this paper, especially Section 7.

https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf

Andrew W. Appel. 2022. Coq’s vibrant ecosystem for verification engineering (Invited paper).

In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22), January 17–18, 2022, Philadelphia, PA, USA.

ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3497775.3503951

[Note, the doi.org link won't start working until mid-January 2022, use the princeton.edu link until then]

Thanks!

This is great! Thanks a lot for writing this piece. Is it still time to report typos?

could be of interest outside the platform stream

Maybe if you report a typo within the next 2 hours . . .

And yes, it should be of interest outside the platform stream, that's why I'm publishing it in CPP.

Andrew Appel said:

Maybe if you report a typo within the next 2 hours . . .

I believe the C semantics used by RefinedC is called Caesium and not Caeserium (in Section 3).

Note to Theo: Thanks for the two typo reports, but one of them is not a typo. "binary tries" is correct. See also this paper:

https://arxiv.org/abs/2110.05063

Efficient Extensional Binary Tries, by A. W. Appel and X. Leroy, 2021

Note to Alix: Thanks for the typo report.

About that paper, I see it benchmarks `cbn`

. Not sure what it exactly mean, but the `cbn`

user facing reduction procedure in coq is call by *name*, while the `lazy`

one is (way more optimized and) call by *need*. Just in case.

**Note:** The correct title of the paper ends with "(Invited Talk)", not "(Invited Paper)". So please cite as,

Andrew W. Appel. 2022. Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk).

In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22), January 17–18, 2022, Philadelphia, PA, USA.

ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3497775.3503951

I did some updates to https://github.com/coq-community/awesome-coq based on projects mentioned in the preprint.

read the preprint a bit closer now, only question mark that came up for me was that the mentioned refinement from MathComp matrices to lists of lists (and then further to Clight) was seemingly done manually? I think that refinement is nowadays available near-automatically via ParamCoq+CoqEAL, but not sure when it was added there.

@Andrew Appel Thanks for the nice overview! Some quick remarks

As you know, both fiat-crypto and bedrock have been useful to construct correct C-programs.

p5. Coq's stdlib classical real numbers are now based on the constructive real numbers.

Computing with constructive real numbers is entirely practical. E.g. the work by Russell O'Connor and my work with @Robbert Krebbers

http://www.springerlink.com/content/m380454267180372/

http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

@Karl Palmskog Good point about CoqEAL. The project seems a bit stalled though...

CoqEAL is maintained and in the Coq Platform (and recently got big additions thanks to porting of ForMath work by Yves Bertot), but I guess it may need more examples and better marketing. One approach is to use it as an incubator for MathComp-related formalization work that then gets integrated into `math-comp`

repo proper.

@Karl Palmskog I meant that I haven't seen it used so much as I expected to see it used.

the relatively low impact of CoqEAL may be partly due to its complex chain of dependencies (MathComp + extensions + ParamCoq), which were rarely available for the latest stable Coq version until now

Another reason could be that it has been nearly abandoned for many years, but it is in better shape now.

Agree, but one recent impressive piece of work that used CoqEAL: https://github.com/math-comp/Apery

Thanks. I didn't know that it was used in Apery!

I guess the integration of param-coq with meta-coq is still waiting on an excited phd-student?

Paramcoq was also recently used here: https://github.com/pi8027/stablesort

Unfortunately the Paramcoq to MetaCoq port may not be very publishable, and may be too complex for a master's thesis, so I have a hard time seeing it happen soon...

Thanks. That seems like a nice use case.

Since real numbers were mentioned, Vincent gave a nice breakdown of how standard library real numbers currently work in Coq here: https://stackoverflow.com/questions/69683736/real-numbers-in-coq

Andrew's very nice keynote talk is now up on YouTube: https://www.youtube.com/watch?v=StQ40osfQTo

Last updated: Apr 14 2024 at 11:02 UTC