Hacker News new | ask | show | jobs
by debugnik 209 days ago
I consider code written in Frama-C as a verifiable C dialect, like SPARK is to Ada, rather than C proper. I find it funny how standard C is an undefined-behaviour minefield with few redeeming qualities, but it gets some of the best formal verification tools around.
2 comments
1718627440 209 days ago
The popular C compilers include a static analyzer and a runtime sanitizer. What features do you consider proper C? The C standard has always been about standardization of existing compilers, not about prescribing features.
link
debugnik 209 days ago
By "static analysis" you mean unsound, best-effort analyzers which try to study code as-is, rarely allow extra annotations, and tolerate false negatives and even positives by design.

While these are a huge improvement over no extra tooling, they don't compare to analyzers like Frama-C plugins, which demand further annotations/proofs if necessary to show code is free of UB, and you can provide further to show your code is not just safe, but correct. Assuming one doesn't ship rejected code, the latter is pretty much its own language with much stronger guarantees, much like SPARK is to Ada.

I like sanitizers and other compiler-specific guarantees, they at least try to fill the gaps by giving proper semantics to UB. But the ones available for C are still insufficient, and some are very resource-heavy compared to just running safe code. I'm excited about Fil-C showing a path forward here.

link
1718627440 208 days ago
Yes, I do. I know they are very different from real correctness verifiers, but it's not like the people only using the compiler has no way of preventing trivial UB bugs. UB also is really only a language concept and nobody is writing code for the abstract C machine.
link
uecker 208 days ago
IMHO and maybe counterintuitively, I do not think the existence of UB makes it harder to do formal verification or have safe C implementations. The reason is that you can treat it as an error if the program encounters UB, so one can either derive local requirements or add run-time checks (such as Fil-C) and then obtains spatial and temporal isolation of memory object.
link