Their 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.
```
I'm super interested how you can do this in C++. Say, I need aggregate struct with a few 16 and 32 bit fields, some are little endian and some big endian. I do not want C++ to let me mix up endianness. How do I do it?
newtypes are not as good as native low level types. after typing a lot of code, one will find out that he needs nightly to get decent integration to avoid casting to low level and back all time.
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.
You can actually do this in C as well. The Windows API has all sorts of handle types that were originally all one type: HANDLE; but by wrapping a HANDLE in various one-member structs were able to derive different handle types that couldn't be intermixed with each other in a type-safe way without some casting jiggery-pokery.
It's just much, much easier and more ergonomic in Ada.
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 regardless
I've never worked in aerospace, however I'm interested in safety-critical software engineering, and I've written a lot of Ada (and written about my experiences with it too). My understanding is that yes you can write safety-critical code in just about any language, but it's much easier to prove conformance to safety standards (like DO-178C, etc.) in Ada than in C++.
I regularly do hobby bare-metal programming in both Ada and C. I find that Ada helps prevent a lot of the common footguns in C. It's not a silver bullet for software safety, but it definitely helps. The point of any programming language is to make doing the right thing easy, and doing the wrong thing hard. All things considered, I think Ada does a good job of that.
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?
> 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?
Which languages remove which classes of bugs entirely? This vagueness is killing me
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...
I found that learning Ada was a good way to learn how to write good C++ code, because both languages are at the same level of abstraction but Ada is clean and opinionated.
The best a example is RAII. This is a pattern in C++ that you have to follow if you don't want to make a mess. In Ada it's a language feature called Controlled Types.
Do you feel the same is true for someone who does mainly rust nowadays ? I had the same feeling with rust & python ; If there are any patterns that help in other languages I'd definitely like to look them up
SPARK is used by NVIDIA for the most secure compute code.
No, just learn C/C++ properly.
I'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 ?
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
https://learn.adacore.com/ - I'd start here, good set of tutorials on the language including some comparative ones. It won't teach you everything you might need to know, but it's a free and good starting point.
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.
Dlang is the GOAT!
Haha, Walter you're definitely not biased on this one. :)
Me? Biased? LOL
If its a personal project then try each and see what you like. Work project then follow your company development guidelines.
Even though it's an Ada ad, 'C*/*C++' vs 'Ada*, *SPARK' is wild.
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.
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?
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.
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.
> If you’re prepared to look at alternative programming languages to avoid the costs and risks of C/C++, SPARK offers an opportunity to go much further than Ada or Rust. SPARK, which is based on Ada, offers industrial-strength formal methods: an opportunity for you to prove mathematically that your software is safe and secure. This paradigm shift in software development methodology offers significant cost savings for high-integrity software.
Forgive me if I sound naive but I always found it a bit weird how something like this is touted as a strength of Ada, but never actually demonstrated in comparison with a heavily typed language like Rust. 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. What you can do in rust, and other languages, is check you're within boundaries and throw an exception if it's out of bounds.
Herein lies the issue: "You can't throw exceptions in this kind of software". True. So how do you prove it WONT go out of bounds at compile time, if the input isn't trusted? Rustacians get picked on a lot for spending more time on type-theory than actually writing working code, but from my perspective it looks worse in Ada, obsessing over proving something in a complete vacuum that can't possibly account for all possible invariants in the real world.
> 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 before it's used.
I wrote about this here: https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...
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 simultaneously" or "in this program state X is always followed by state Y".
This is super useful for safety systems, because you can express safety in these kinds of functions that are falsifiable by the proof system. E.g: "the ejection seat is only engaged after the cockpit window is ejected" or "if the water level exceeds X the pump is always active within 1 minute".
C++ is a good alternative to "C/C++"
yes, you should.
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 complain about its ties to Apple, but hopefully with it gaining much wider cross-platform support, it may not matter that much in the future, but I guess it remains to be seen.
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.
(2024)