Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Should I choose Ada, SPARK, or Rust over C/C++? (2024)

blog.adacore.com

Post reply on HN
Print view View original

51–60 of 173 posts

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#51

Post by smj-edison »

jandrewrogers wrote: post #32
jdougan wrote: post #9

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 ot…

> 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.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#52

Post by waterTanuki »

vouwfietsman wrote: post #45
ajxs wrote: post #41

Earlier quoted context omitted.

> Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time. > ...but from my perspective it looks worse in Ada... This isn't really true. SPARK obviously can't prove that the input will be valid, but it can formally prove that the validity of the user input is verified…

I am no expert here what I remember is mostly from CS courses, but isn't the entire point of a formal program proof that you can reason about the combinatorics of all data and validate hypothesis on those? It's one thing to say: "objects of this type never have value X for field Y", or "this function only works on type U and V", but its a lot more impressive to say "in this program state X and Y are never achieved si…

But isn't the entire point of rust's verbose type system to declare valid states at compile time? I don't exactly see how this can't be proved in rust.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#53

Post by morshu9001 »

School-Cotton wrote: post #14
crims0n wrote: post #11

Alternatively, just get better at C/C++… It isn’t going anywhere, and it feels like more developers are coming around to the idea that maybe security guarantees are not worth throwing the baby out with the bath water.

It’s a common misconception that the point of Rust is just security. Rust helps avoid a very broad class of bugs, that security bugs are only a subset of.

I'd rather use Rust even if safety weren't a concern. Basically for all the reasons Torvalds doesn't like C++ but is fine with Rust.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#54

Post by [deleted] »

ranger_danger wrote: post #12

Personally I think Swift can be a good choice that is more familiar to existing C++ developers than the others, and a lot of people seem to be sleeping on it. It has full native interop with C and C++ so you can already use all your existing libraries. Historically it lacked cross-platform support but this is not true anymore. It does lack a native GUI framework, but for now you can keep using C++ ones. Some people c…

[deleted]

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#55

Post by morshu9001 »

echelon wrote: post #29
School-Cotton wrote: post #14

Earlier quoted context omitted.

It’s a common misconception that the point of Rust is just security. Rust helps avoid a very broad class of bugs, that security bugs are only a subset of.

Google had published a few papers stating that Rust code has fewer defects than similar complexity Go and Java services. It's not just memory safety, but the design of the type system and error handling semantics that enable it to be smooth with exceptional behavior.

Go's biggest flaw for backends is the error handling. No exceptions and nothing checking that you use the err.

Java's issue might be the lack of cooperative multitasking until recently (virtual threads). Best you could do was those promises frameworks that mangle your code, and Google in particular uses something a hundred times worse called Guice (which is also DI).

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#56

Post by AlotOfReading »

oguz-ismail wrote: post #46
AlotOfReading wrote: post #42

Earlier quoted context omitted.

Safe Rust and Ada SPARK entirely remove classes of bugs like undefined behavior and memory safety issues. The latter will also statically eliminate things like overflow and type range errors. These are subsets of their respective languages, but all safety critical development in C and C++ relies on even more constrained language subsets (e.g. MISRA or AV++) to achieve worse results.

> These are subsets of their respective languages, but Pretty much every language has such a subset. Nothing new then, sigh...

C and C++ don't have such a subset. That seems pretty relevant, given they're the languages being compared and they're used for the majority of safety critical development.

The standards I mentioned use tricks to get around this. MISRA, for example, has the infamous rule 1.3 that says "just don't do bad things". Actually following that or verifying compliance are problems left completely to the user.

On the other hand, Safe Rust is the default. You have to go out of your way to wrap code in an unsafe block. That unsafe block doesn't change the rules of the language either, it just turns off some compiler checks.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#57

Post by zppln »

ecshafer wrote: post #22
firesteelrain wrote: post #7

I know there is a belief that Rust/Ada etc is safer than C/C++ and in some cases that is true. I know of multiple, airworthy aircraft that are flying with C++ code. I also know of aircraft flying with Ada. The aircraft flying with Ada is hard to maintain. There is also a mountain of testing that goes into it that is not just unit testing. This mountain of integration, subsystem and system level testing is required re…

It is not saying that it is not possible to make C code that is safe enough to be on an airplane. Its that there are languages with additional features which make it easier to have a high confidence. If you can remove entire classes of bugs automatically, why not do so?

It matters less than you think. The entire point of e.g. DO-178C is to achieve high assurance that the code performs it's intended function. Basically, you need to be able to trace your object code to system level requirements. You need to achieve 100% MC/DC coverage from requirements based testing. If there's something you don't cover you either remove the code, or add derived requirements (which need to be assessed by the systems safety process). Language choice doesn't remove any of the objectives you need to achieve.

Also, keep in mind that the desire to have a deterministic system puts a lot of constraint on what kind of behavior you can program anyway.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#58

Post by Agingcoder »

jandrewrogers wrote: post #32
jdougan wrote: post #9

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 ot…

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.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#59

Post by Agingcoder »

lenkite wrote: post #35
Jtsummers wrote: post #31

Earlier quoted context omitted.

Yes, you can mix and match the two. This lets you do things like build a library with SPARK for some critical portion where you want SPARK's guarantees and can accept its limitations, and incorporate it into an application built with the rest of Ada.

Oh lovely - need to put Ada on the learning plan. Formal languages were a bit of a drag because you needed to maintain a separate "specification" copy of your critical code. Going through Ada sample programs and surprised I can grok stuff without knowing anything about the language. Wondering why it never took off in the standard software world. Sure its a bit verbose, but so are Java and MacOS API's

I think at least slow and expensive compilers back in the days, the defense and aerospace stigma, and in more recent times a common misperception that it’s closed source. And it’s never been cool stuff.

And yes you’re right, it’s a very good language.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#60

Post by blub »

ecshafer wrote: post #22
firesteelrain wrote: post #7

I know there is a belief that Rust/Ada etc is safer than C/C++ and in some cases that is true. I know of multiple, airworthy aircraft that are flying with C++ code. I also know of aircraft flying with Ada. The aircraft flying with Ada is hard to maintain. There is also a mountain of testing that goes into it that is not just unit testing. This mountain of integration, subsystem and system level testing is required re…

It is not saying that it is not possible to make C code that is safe enough to be on an airplane. Its that there are languages with additional features which make it easier to have a high confidence. If you can remove entire classes of bugs automatically, why not do so?

Here’s an example how safety-critical C is written and formally verified: https://www.absint.com/

Based on what I know about Rust, it’s harder to write Rust to that same level of confidence, but I haven’t kept up with their safety-critical initiative.

Post reply on HN