[Waterluvian]

This is way outside my domain but isn’t the answer: yes, if the code is formally proven safe?

Doesn’t NASA have an incredibly strict, specific set of standards for writing safety critical C that helps with writing programs that can be formalized?

[okanat]

There are safety recommendations / best practice standards like CERT. None of them will prevent you from making intentional looking but logically unsound memory unsafe operations with C and C++. The code can be very indistinguishable from safe code. The things that C and C++ allow you to do basically makes code written in those languages impossible to fully formally prove. Although there are subsets, the basic integer operations and primitive types are messed up with C. So without uprooting how basic integer and pointer types work, it is impossible to make C and C++ safer. Such change will make all C and C++ programs invalid.

C and C++ always defaults to minimum amount of safety for maximum allowance of the compiler interpretation. The priority of the language designers of them is keeping existing terrible code running as long as possible first, letting compilers interpret the source code as freely as possible second.

That's why many military and aerospace code actually uses much safer and significantly more formally verifiable Ada.

[uecker]

There is also a lot of formally verified in C.

[spookie]

> impossible to formally prove

If you assume the entire lang, yes. If you use a large subset, no. Furthermore, compiler interpretation might actually be sane! There are more compilers out there than GCC, Clang or MSVC. I suspect many assumptions are being made on this claim.

[Waterluvian]

Thanks for explaining that. It really fills in a lot for me.

[arto]

https://david-haber.github.io/posts/the-right-stuff/