Hacker GitHub

← All repos

AbsInt/CompCert

View on GitHub ↗ ★ 2,267 Rocq Prover

The CompCert formally-verified C compiler

22 mentions on Hacker News by 17 people: 2 stories, 20 comments · first 2015-04-05 · latest 2026-07-05

Mentions per year 22 mentions · busiest year 2017 (5)
20082026
AllStoriesComments NewestTopOldest
  1. …pass. CompCert apparently has 1200LoC of proving DCE, one of the simplest whole-function passes - https://github.com/AbsInt/CompCert/blob/02fc017cf69210db5fd5...
    comment by dzaima · 2026-07-05 · in It's not me, it's the compiler
  2. …Coq shares this property for instance, and you can write an optimizing C compiler in Coq: https://github.com/AbsInt/CompCert .
    comment by octachron · 2022-12-16 · in Proofs about Programs
  3. …to write some formally verified C, you can check out Frama-C [3]. [1] https://sel4.systems/ [2] https://github.com/AbsInt/CompCert [3] https://frama-c.com/
    comment by naasking · 2022-10-29 · in BearSSL: A smaller SSL/TLS library
  4. …not yet near graduation, I suggest to do a compiler related internship. [1] https://cakeml.org/ [2] https://github.com/AbsInt/CompCert
    comment by GregarianChild · 2022-08-25 · in Ask HN: How to get a job as a compiler engineer?
  5. …ub.com/gcc-mirror/gcc/tree/master/gcc/config Compare with CompCert, the formally verified C compiler: https://github.com/AbsInt/CompCert Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully…
    comment by dandotway · 2022-01-02 · in Why the C Language Will Never Stop You from Making Mistakes
  6. …2. CompCert, a formally verified C compiler, is implemented using OCaml and Coq: https://github.com/AbsInt/CompCert Nothing at this level yet exists in the Rust and Zig ecosystems, for example. Rust is a very complicated language with many
    comment by dandotway · 2021-10-04 · in Multicore OCaml: September 2021, effect handlers will be in OCaml 5.0
  7. …they attempted to switch to LGPL to fix that two months ago[1], but perhaps missed some parts. [1] https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...
    comment by tyingq · 2021-06-27 · in CompCert – Formally-verified C compiler
  8. …open-source projects such as VST ( http://vst.cs.princeton.edu/ ) that connect with CompCert. at https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.
    comment by alfu · 2021-06-27 · in CompCert – Formally-verified C compiler
  9. …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…
    comment by exikyut · 2021-06-27 · in CompCert – Formally-verified C compiler
  10. …than me. I found a lot of the source code to CompCert C (a verified C compiler) illuminating: https://github.com/AbsInt/CompCert However, it will be difficult to understand without doing Software Foundations first (I still find personally…
    comment by ojnabieoot · 2020-10-27 · in Homotopy Type Theory (2012) [pdf]
  11. …methods can be partially applied to produce provably more correct code (in some metrics). [1] https://github.com/AbsInt/CompCert
    comment by lifthrasiir · 2018-09-12 · in SQLite: Infinite loop due to the ‘order by limit’ optimization
  12. …of such values. For whatever it's worth, the author's solution for bytes is the same as CompCert's: https://github.com/AbsInt/CompCert/blob/3939a1ccfdb86795e9fd...
    comment by tom_mellior · 2018-07-26 · in Pointers Are Complicated, or What’s in a Byte?
  13. …realm. Take a look at the ideal mathematical (verified) C compiler written in Coq. I find it neat: https://github.com/AbsInt/CompCert
    comment by ernst_klim · 2018-07-12 · in Unix system programming in OCaml (2014)
  14. https://github.com/AbsInt/CompCert/issues/211
    comment by based2 · 2017-12-19 · in CompCert: verified compiler for a large subset of the C
  15. …but everything is also variously covered by the GPL (v2 or later), LGPL v3, and BSD 3-clause. Ref: https://github.com/AbsInt/CompCert/blob/master/LICENSE I'm curious if I could use this in a commercial setting if I perfectly comply with…
    comment by exikyut · 2017-08-05 · in Ask HN: What tech that's right around the corner are you most excited about?
  16. …* coq https://github.com/coq/coq * flow https://github.com/facebook/flow * CompCert https://github.com/AbsInt/CompCert * frama-c https://github.com/Frama-C * 0install https://github.com/0install/0install
    comment by ernst_klim · 2017-07-16 · in A deep dive into Multicore OCaml garbage collector
  17. …parser for C: http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf The result is in CompCert: https://github.com/AbsInt/CompCert/tree/master/cparser
    comment by tom_mellior · 2017-06-29 · in Writing Parsers Like it is 2017 [pdf]
  18. …never implemented. [1] The bug fix is to stop using GCC for sensitive code. Use CompCert instead. https://github.com/AbsInt/CompCert [0] http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1381.pdf [1] https://sourceware.org/ml/libc-alpha/2014…
    comment by eliteraspberrie · 2016-01-18 · in Things I learned from OpenSSH about reading very sensitive files
  19. It exists. It's called CompCert. https://github.com/AbsInt/CompCert It's free for non-commercial use. I've used it for several months now to build things like Tor. I haven't noticed any disadvantage compared to GCC or Clang.
    comment by eliteraspberrie · 2015-12-21 · in Boringcc: Proposal for a C compiler for secure software
  20. …OpenBSD is no run of the mill *nix, either. http://compcert.inria.fr/compcert-C.html EDIT: See also https://github.com/AbsInt/CompCert
    comment by cantankerous · 2015-04-05 · in Compilers in OpenBSD (2013)