CompCert

The CompCert formally-verified C compiler (by AbsInt)

CompCert Alternatives

Similar projects and alternatives to CompCert

  • GitHub repo Mumble

    Mumble is an open-source, low-latency, high quality voice chat software.

  • GitHub repo coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

  • Scout APM

    Scout APM: A developer's best friend. Try free for 14-days. Scout APM uses tracing logic that ties bottlenecks to source code so you know the exact line of code causing performance issues and can get back to building a great product faster.

  • GitHub repo wuffs

    Wrangling Untrusted File Formats Safely

  • GitHub repo checkedc

    Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.

  • GitHub repo winix

    A UNIX-style Operating System for the Waikato RISC Architecture Microprocessor (WRAMP)

  • GitHub repo cakeml

    CakeML: A Verified Implementation of ML

  • GitHub repo silt

    An in-progress fast, dependently typed, functional programming language implemented in Swift.

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

NOTE: The number of mentions on this list indicates mentions on common posts. Hence, a higher number means a better CompCert alternative or higher similarity.

Suggest an alternative to CompCert

Posts

Posts where CompCert has been mentioned. We have used some of these posts to build our list of alternatives and similar projects - the last one was on 2021-06-27.
  • Proof Assistant Makes Jump to Big-League Math | Quanta Magazine
    reddit.com/r/math | 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.
  • Hacker News top posts: Jun 27, 2021
    A Proven Correct C Compiler\ (76 comments)
  • A Proven Correct C Compiler (Used by Airbus)
    news.ycombinator.com | 2021-06-26
    As noted in the License section of the readme,

    > CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support and extra features, can be purchased from AbsInt. See the file LICENSE for more information.

    However, https://github.com/AbsInt/CompCert/blob/master/LICENSE goes onto say that

    > The following files in this distribution are dual-licensed both under

    news.ycombinator.com | 2021-06-26
    On their website, the claim is more ambitious: "The main result of the project is the CompCert C verified compiler, a high-assurance compiler for _almost all_ of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors." (https://compcert.org/)
    news.ycombinator.com | 2021-06-26
    >The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that they can be used together with the rest of CompCert (the implementation of the compiler, so to speak), which is NCL-only.

    >Additionally, the interface files in question are also licensed under the GPL so that they can be used in other, open-source projects such as VST (http://vst.cs.princeton.edu/) that connect with CompCert.

    at https://github.com/AbsInt/CompCert/issues/140 (2016)

    news.ycombinator.com | 2021-06-26
  • CompCert C a formally verified optimizing compiler for a large subset of C99
    news.ycombinator.com | 2021-06-26
  • Automatically Make Unit Tests
    news.ycombinator.com | 2021-05-19
  • Phantom types in Swift
    reddit.com/r/swift | 2021-02-17
    Yes, it is a false dichotomy to suggest one does not need tests because one has types. One needs both in systems of sufficient complexity. Even CompCert has a test suite, and it’s got a full formal proof of its own correctness!

Stats

Basic CompCert repo stats
10
1,274
7.9
8 days ago

AbsInt/CompCert is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.