[dead]
Should I choose Ada, SPARK, or Rust over C/C++? (2024)
21–30 of 173 posts
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#22I 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?
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#23I'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.
Zig is not memory safe at all
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#24Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#25Their example of why Ada has better strong typing than Rust is that you can have floats for miles and floats for kilometers and not get them mixed up. News flash, Rust has newtype structs, and you can also do basically the same thing in C++. I don't know much about Ada. Is its type system any better than Rust's?
This was posted to about a day ago:
https://github.com/johnperry-math/AoC2023/blob/master/More_D...
But a noteworthy excerpt: ```
Ada programs tend to define types of the problem to be solved. The compiler then adapts the low-level type to match what is requested. Rust programs tend to rely on low-level types.
That may not be clear, so two examples may help:
Ada programmers prefer to specify integer types in terms of the ranges of values they may take and/or the precision of floating-point types in terms of digits. I ended up doing this at least once, where on Day 23 I specified a floating-point type in terms of the number of digits it should reproduce accurately: Digits 18. The compiler automatically chose the most appropriate machine type for that.
Ada arrays don't have to start from 0, nor even do they have to be indexed by integers. An example of this appears below.
```
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#26Earlier quoted context omitted.
It's basically a subset of Ada, so you can use it anywhere you'd use Ada. I don't think Lean is at a point that it's an Ada replacement.
Lean the math prover? What does that have to do with Ada/Rust?
> Lean the math prover? What does that have to do with Ada/Rust?
I'm going to be rude, but there are 4 sentences in this thread and you appear to have not read two of them.
The comment I responded to:
>> I've never heard of SPARK. What advantages does it have compared to Lean? [emphasis added]
The "It" in my response refers to SPARK.
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#27Their example of why Ada has better strong typing than Rust is that you can have floats for miles and floats for kilometers and not get them mixed up. News flash, Rust has newtype structs, and you can also do basically the same thing in C++. I don't know much about Ada. Is its type system any better than Rust's?
Yes and no, you need to look deeper into Ada to find that it can have compile time guarantees higher than what you can get from a struct named km and miles.
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#28Personally 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…
Swift, while being slightly more friendly for extreme beginners than rust, is just so kneecapped and bloated that it has the opposite problem as rust. At some moderate level of competence it actively hinders learning. All of the weird closure and multithreading syntax is more harmful than good. Whereas Rust has a high floor and somewhat infuriating borrow checking, once you figure your way out of them you’ve actually learned a lot about how computers work along the way.
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#29Alternatively, 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.
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.
Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)
#30I've never heard of SPARK. What advantages does it have compared to Lean?
It's basically a subset of Ada, so you can use it anywhere you'd use Ada. I don't think Lean is at a point that it's an Ada replacement.
In a project, can you develop one module in Ada and another in SPARK and compile them together ? So, you can use safety-critical code in one module and regular Ada code in other modules ?