OCoctachron·Dec 16, 2022
This is a common property for proof-oriented languages. Coq shares this property for instance, and you can write an optimizing C compiler in Coq: https://github.com/AbsInt/CompCert .
In Proofs about ProgramsAbsInt
CompCert
Rocq Prover2015–2026
AbsInt / CompCert
CompCert
The CompCert formally-verified C compiler
17Distinct people
22Mentions
0Explicit recommenders
2.3KGitHub stars
What to know before exploring
What it is
The CompCert formally-verified C compiler
GitHub
Where it is used
No documented product use was verified in the last source check.
What people are saying
No recommendation phrase was found in the indexed comments.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 8–Nov 15 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/15/2026, 9:02:44 AM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year22 dated mentions
Observed mentions: 2015-04-05 00:38:10 UTC to 2026-07-05 18:33:23 UTC.
* An incomplete calendar period is marked with an outlined bar. Its count is not directly comparable with a full period.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2015 | 2015-01-01 00:00:00 UTC | 2016-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2016 | 2016-01-01 00:00:00 UTC | 2017-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2017 | 2017-01-01 00:00:00 UTC | 2018-01-01 00:00:00 UTC | 5 | 1 | 4 |
| 2018 | 2018-01-01 00:00:00 UTC | 2019-01-01 00:00:00 UTC | 3 | 0 | 3 |
| 2019 | 2019-01-01 00:00:00 UTC | 2020-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 5 | 1 | 4 |
| 2022 | 2022-01-01 00:00:00 UTC | 2023-01-01 00:00:00 UTC | 4 | 0 | 4 |
| 2023 | 2023-01-01 00:00:00 UTC | 2024-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2024 | 2024-01-01 00:00:00 UTC | 2025-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2025 | 2025-01-01 00:00:00 UTC | 2026-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2026 (partial) | 2026-01-01 00:00:00 UTC | 2027-01-01 00:00:00 UTC | 1 | 0 | 1 |
What Hacker News says
4 sourcesDepends what you mean by "popular". seL4 [1] is formally verified, open source and is used as baseband firmware in millions of phones, among other uses. Google just recently started an embedded OS based on it as well.
CompCert [2] is a formally verified optimizing C compiler.
Most formal verification happens in compilers or low-level mission critical systems due to the cost.
If you want 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/
In BearSSL: A smaller SSL/TLS libraryI'm a bit surprised by what you write.
Until recently I was heading a compiler team. We found it impossible to hire experienced compiler engineers despite paying very well, so we essentially switched to
hiring promising university graduates and trained them on the job. My peers in other companies are all in the same situation.
Note that there is a mismatch between academic and industrial compiler work. A university compilers course is necessary, but not sufficient to be considered experienced, you should have good knowledge of things like
ABI design, ELF, DWARF, LLVM's tablegen, C++, compilation of varargs etc. This stuff
is not typically taught in compiler courses (for good reason, since it is a bit arbitrary) but it is absolutely vital to producing a working, industrial strength compiler.
You should also have some idea about computer
Read the rest
architecture, so you can read ISA manuals and understand what individual machine instructions do, and what performance characteristics they have. Otherwise you won't be able to write good instruction selection and scheduling. Given the increasing prevalence of JIT compilers (eg eBPF in the Linux kernel), it's also useful to know about that. Another dimension is security: modern compilers to need to worry about stack canaries, shadow stacks etc. This too is not taught at universities.
Regarding what tool/library/framework, skills are rather transferrable, so I would not worry too much about this. LLVM is by far the most widely used open framework and is easier to get into than other open stuff. If you are knowledgable about security and verification, doing hacking on e.g. CakeML [1] or CompCert [2] might be interesting.
A good way of being hired is to go to e.g. LLVM or GCC meetup, and make it clear that you are looking for a job.
Put it on your Github that you are looking for a job. Put a link to an LLVM or GCC (or similar) compiler phase that you have written. The next LLVM dev meeting is November 8-9 in San Jose, CA, hang out there, rest assured there will be many companies seeking to hire. Bonus points if you give a presentation, even if it's whimsy like compiling Brainfuck to Intel 4004 ... Another avenue is RISCV startups which are currently 10-a-penny, they all need and hire compiler engineers. Cold-contact them ...
PS, since you are a PhD student. I suggest finishing your PhD in some form or other. A lot of companies are loath to hire PhD students before they finish, or make the job offer contingent upon successful graduation. That certainly was our policy. If you are not yet near graduation, I suggest to do a compiler related internship.
[1] https://cakeml.org/
[2] https://github.com/AbsInt/CompCert
I've used SPARK with GNAT Studio, I've used Frama-C, and I'm also experimenting with CBMC. Frama-C is way more powerful than SPARK, but also consequently has a much deeper learning curve.
SPARK does not allow doubly linked lists:
https://blog.adacore.com/pointer-based-data-structures-in-sp...
For example, singly-linked lists and trees are supported whereas
doubly-linked lists are not.
With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.
However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a
Read the rest
billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.
AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:
https://github.com/AdaCore/why3
And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:
https://github.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 utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:
https://softwarefoundations.cis.upenn.edu/