Coq compcert

Open-source Coq projects categorized as compcert | Edit details

Coq compcert Projects

  • GitHub repo CompCert

    The CompCert formally-verified C compiler

    Project mention: Proof Assistant Makes Jump to Big-League Math | Quanta Magazine | | 2021-07-29

    Again, the answer is "it depends"; there's even fragmentation between Lean3 and Lean4. Coq is very good at many things, such as verified compilers whilst Lean3 could never dream of such things. Lean4 is written in Lean4 so there's some hope for that. Meanwhile, a lot of maths has been written in both and they're both still actively used; I personally prefer Lean but that's personal preference. A "good" baseline to see mathematical progress in various proof assistants is Freek's 100 theorem list.

NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020). The latest post mention was on 2021-07-29.


Project Stars
1 CompCert 1,274