Skip to content

Comment on C*: Unifying Programming and Verification in C (2025)

Comments

I suspect that there is a body of C programmers out here that use C on a regular basis that aren’t posting who know that using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done.

They don’t reply to these threads to share that knowledge because these threads devolve into cesspools about how you should just use Rust despite the language not meeting specific requirements authors have that you have to do additional work and maintenance for in “safe” languages that you get for free in C because you don’t have to emulate it.

I suspect that there is a body of C programmers out here that use C on a regular basis that aren’t posting who know that using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done.

C* (the submitted language) is not just about determining memory correctness and related program features like what Valgrind will do for you (or help with). It's about proving correctness of programs more generally, so any C programmer not looking at it because they know about Valgrind are choosing to skip something interesting for a very poor reason.

    using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done
I wish that were the case, but it's not. Dynamic analyzers are fantastic and everyone should be using them constantly, but they don't solve the problem of UB. They tell you whether your code, as translated by a specific compiler using a specific set of flags today has detectable problems. There are still gaps, and what's true today might not be true even for the same source code built tomorrow, or given different inputs. Asserting my safety-critical code does X or Y is important to me, and neither C nor C++ have standard tooling that fully addresses that need.

Other languages are much farther along than this. You can in theory take a pile of Rust and isolate exactly the points where undefined behavior might occur, or eliminate them entirely in Ada/Spark.

I suspect that there is a body of C programmers out here that use C on a regular basis that aren’t posting who know that using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done.

Absolutely right! I sincerely hope they share their knowledge here and elsewhere.

They don’t reply to these threads to share that knowledge because these threads devolve into cesspools

HN is often rage-inducing when it comes to comments on C/C++/Fortran/Cobol/etc. older languages and systems. There are many critical and industrial-strength systems developed by the previous generation of engineers/programmers which today's noobs/cargo-cultists cannot even hope to imagine much less understand.

As an example, people talk about all the great features provided by Erlang but forget that its BEAM VM where most of the "magic" resides is actually written in C! Imagine how much expertise lies buried in its implementation!

That is called Trusted Computing Base in security speech, having ensure Erlang runtime implementation is safe, is a much reduced effort than certifying a telecommunications distributed application 100% written in C as equally safe under the same attack vectors.

Security Standards/Frameworks like "TCB" (https://en.wikipedia.org/wiki/Trusted_computing_base), "Common Criteria" (https://en.wikipedia.org/wiki/Common_Criteria) etc. are not what i am talking about here. I am pointing to the fact that there is a large piece of industrial-strength C code (i.e. BEAM/ERTS) whose architecture/complexity/techniques are manifested as the "features" of another higher-level language (i.e. Erlang). People seem to appreciate the latter while not comprehending the former. The underlying C-based infrastructure is so good that there are now multiple different-paradigm languages targeting the BEAM.

Incidentally, the C implementation of BEAM/ERTS is not formally verified; only some parts of the upper-layer intermediate representation and bytecode have been verified (academic). Also an Erlang distributed cluster was designed to operate only within an already secure network (i.e. telephone network) and not on today's public Internet. So if you want to run Erlang securely you would need to know overall system security architectures and follow advice given by the "Erlang Ecosystem Foundation Security Working Group" - https://security.erlef.org/

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.