[pkhuong]

> Just don't use C for sending astronauts in space

But do use C to control nuclear reactors https://list.cea.fr/en/page/frama-c/

It's a lot easier to catch errors of omission in C than it is to catch unintended implicit behavior in C++.

[debugnik]

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.

[1718627440]

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.

[uecker]

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.