Skip to content

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

Comments

    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.

AboutSource Built by g1lg1l

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