The CompCert formally-verified C compiler
Check out CompCert C compiler. It's your usual C compiler but with all optimizations verified to be correct (i. e. not changing program semantics). This means that as long as you agree with definition of program semantics given in the compiler (it's reasonable) and believe that Coq - the dependently typed language behind CompCert - is correct, you can be sure that no optimization breaks your code and that's a big deal since program optimization algorithms are very prone to bugs in usual compilers.
Ask HN: Can the same individual accomplish more with programming than proofs?
1 project | news.ycombinator.com | 14 Apr 2022
1 project | reddit.com/r/ProgrammerHumor | 15 Feb 2022
Writing a Fuzzer for NES Games
1 project | news.ycombinator.com | 27 Nov 2021
Multicore OCaml: September 2021, effect handlers will be in OCaml 5.0
1 project | news.ycombinator.com | 4 Oct 2021
Coverage Is Not Strongly Correlated with Test Suite Effectiveness
1 project | news.ycombinator.com | 28 Sep 2021