Coq Compiler

Open-source Coq projects categorized as Compiler

Top 3 Coq Compiler Projects

  • CompCert

    The CompCert formally-verified C compiler

  • Project mention: Differ: Tool for testing and validating transformed programs | news.ycombinator.com | 2024-01-31

    A big problem is that proving that transformations preserve semantics is very hard. Formal methods has huge potential and I believe it will be a big part of the future, but it hasn't become mainstream yet. Probably a big reason why is that right now it's simply not practical: the things you can prove are much more limited than the things you can do, and it's a lot less work to just create a large testsuite.

    Example: CompCert (https://compcert.org/), a formally-verified compiler AKA formally-verified sequence of semantics-preserving transformations from C code to Assembly. It's a great accomplishment, but few people are actually compiling their code with CompCert. Because GCC and LLVM are much faster[1], and have been used so widely that >99.9% of code is going to be compiled correctly, especially code which isn't doing anything extremely weird.

    But as articles like this show, no matter how large a testsuite there may always be bugs, tests will never provide the kind of guarantees formal verification does.

    [1] From CompCert, "Performance of the generated code is decent but not outstanding: on PowerPC, about 90% of the performance of GCC version 4 at optimization level 1"

  • jasmin

    Language for high-assurance and high-speed cryptography (by jasmin-lang)

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo
  • unbound

    Replib: generic programming & Unbound: generic treatment of binders

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).

Coq Compiler related posts

Index

What are some of the best open-source Compiler projects in Coq? This list will help you:

Project Stars
1 CompCert 1,761
2 jasmin 222
3 unbound 44

Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com