Comment by keyle
6 hours ago
I don't understand this passion for turning C into what it's not...
Just don't use C for sending astronauts in space. Simple.
C wasn't designed to be safe, it was designed so you don't have to write in assembly.
Just a quick look through this and it just shows one thing: someone else's walled garden of hell.
> 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++.
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.
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.
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.
2 replies →
> Just don't use C for sending astronauts in space. Simple.
Last time I checked, even SpaceX uses C to send astronauts to space...
Some C devs will make all kinds of crazy efforts only not to use C++.
C++ is edge case hell even for simple looking code
Not really, only in the mind of haters.
1 reply →
I agree, if people just had refrained from building things in c/c++ that operated on data from across a security boundary we wouldn't be in this mess.
Actually C performs quite good in exactly that area.
https://ntrs.nasa.gov/citations/19950022400
And
https://hackaday.com/2024/02/10/the-usage-of-embedded-linux-...