I'm not sure I'd want to limit the selection of languages that much. Depending on the project and how much language risk you can manage (as opposed to security risk), there also is D, Odin, and Zig. And probably a bunch more I'm unfamiliar with.
I'm not sure I'd want to limit the selection of languages that much. Depending on the project and how much language risk you can manage (as opposed to security risk), there also is D, Odin, and Zig. And probably a bunch more I'm unfamiliar with.
Most of what gives high-reliability or high-assurance code that label is the process rather than the language. In colloquial terms it rigorously disallows sloppy code, which devs will happily write in any language given the chance.
As much as C is probably the least safe systems language, and probably my last choice these days if I had to choose one, more high-assurance code has probably been written in C than any other language. Ada SPARK may have more but it would be a close contest. This is because the high-assurance label is an artifact of process rather than the language.
Another interesting distinction is that many formalisms only care about what I would call eventual correctness. That is, the code is guaranteed to produce the correct result eventually but producing that result may not be produced for an unbounded period of time. Many real systems are considered “not correct” if the result cannot be reliably delivered within some bounded period of time. This is a bit different than the classic “realtime systems” concept but captures a similar idea. This is what makes GCs such a challenge for high-reliability systems. It is difficult to model their behavior in the context of the larger system for which you need to build something resembling a rigorous model.
That said, some high-assurance systems are written in GC languages if latency is not a meaningful correctness criterion for that system.
If I was writing a high-reliability system today, I’d probably pick C++20, Zig, and Rust in that order albeit somewhat in the abstract. Depending on what you are actually building the relative strengths of the languages will vary quite a bit. I will add that my knowledge of Zig is more limited than the other two but I do track it relatively closely.
I don’t understand how you can get the same kind of reliability with C than with Spark - process or not, a formal proof is a formal proof. That’s much harder to get with C.
Why is it harder?
> Most of what gives high-reliability or high-assurance code that label is the process rather than the language.
This is what I've heard too. I have a friend who works in aerospace programming, and the type of C he writes is very different. No dynamic memory, no pointer math, constant CRC checks, and other things. Plus the tooling he has access to also assists with hitting realtime deadlines, JTAG debugging, and other things.
> no pointer math
How does that work out? Does he never uses arrays and strings?
Like in most languages, with indexes.
But in C that's just syntax sugar for pointer math.
It still makes it possible to have bounds checking. (And it is also not true anymore for C2Y.)
Except it is more obvious what is the intention, it is about clarity to the reader.
My point was indeed, that if you don't use pointer arithmetic in C, that means that you don't use arrays. I mean when you declare arrays of a fixed size, you can also declare an equivalent number of primitive variables instead, but I would find that inconvenient. Hence the question.
If I remember correctly, he meant that only array accesses are used, because their length can be checked (as all arrays have a static length due to no dynamic memory).
Indeed, this is what many people do. But even if you use dynamic memory, if you replace pointer arithmetic by array indexing, you get bounds checking. And in C this also works for arrays of run-time length.
But can't I put any pointer arithmetic in array brackets, so it wouldn't limit anything?
Zig is not memory safe at all
Nor is any other dime-a-dozen LLVM frontend with basically the same bullshit syntax. What is your point?
swift and rust?
What about them?
they are memory safe
Proof?