A Proven Correct C Compiler (Used by Airbus)

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • SonarLint - Deliver Cleaner and Safer Code - Right in Your IDE of Choice!
  • Scout APM - Less time debugging, more time building
  • SaaSHub - Software Alternatives and Reviews
  • CompCert

    The CompCert formally-verified C compiler

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

  • cakeml

    CakeML: A Verified Implementation of ML

    CakeML[0] is another formally verified compiler. Notably, unlike compcert, it is open source.

    The language it implements (an sml dialect) is high-level and garbage collected, meaning that it is not usable in all of the same domains, but work is ongoing to reuse much of the compiler infrastructure for 'pancake', a low-level language.

    0. https://github.com/CakeML/cakeml

  • SonarLint

    Deliver Cleaner and Safer Code - Right in Your IDE of Choice!. SonarLint is a free and open source IDE extension that identifies and catches bugs and vulnerabilities as you code, directly in the IDE. Install from your favorite IDE marketplace today.

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

  • wuffs

    Wrangling Untrusted File Formats Safely

    I don't agree.

    Consider WUFFS https://github.com/google/wuffs

    WUFFS will give you a C library that can turn PNG data into raw image data and is definitely correct. It's not exactly idiomatic C, you'd assume if a person wrote this code it's probably wrong, but WUFFS promises it's correct. CompCert should turn that C library into executable code which is therefore also definitely correct.

    Now, maybe you will screw up code that reads the PNG data from a disk file, or draws the image on a screen, or a million other things, but the WUFFS library components are definitely fine, not just "Bill wrote it and he's got 20 years experience" fine or "It passed the unit tests" fine but "Four Color Theorem" fine.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts