9 ms·
Should I choose Ada, SPARK, or Rust over C/C++? (2024)
- phibz 1y agoIf its a personal project then try each and see what you like. Work project then follow your company development guidelines.
- jordanb 1y agoI 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.
- alberth 1y ago(2024)
- mcdonje 1y agoEven though it's an Ada ad, 'C*/*C++' vs 'Ada*, *SPARK' is wild.
- firesteelrain 1y agoI 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
- ajxs 1y agoI'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.
- ecshafer 1y agoIt 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?
- oguz-ismail 1y ago> 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
- AlotOfReading 1y agoSafe 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.
- oguz-ismail 1y ago
- usamoi 1y agoI've never heard of SPARK. What advantages does it have compared to Lean?
- Jtsummers 1y agoIt'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.
- adastra22 1y agoLean the math prover? What does that have to do with Ada/Rust?
- Jtsummers 1y ago> 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.
- adastra22 1y agoThere was no need to be rude.
- lenkite 1y agoIn 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 ?
- Jtsummers 1y agoYes, 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.
- jdougan 1y agoI'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.
- iknowstuff 1y agoZig is not memory safe at all
- oguz-ismail 1y agoNor is any other dime-a-dozen LLVM frontend with basically the same bullshit syntax. What is your point?
- kobebrookskC3 1y agoswift and rust?
- oguz-ismail 1y agoWhat about them?
- kobebrookskC3 1y agothey are memory safe
- casey2 1y agoProof?
- jandrewrogers 1y agoMost 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.
- on_the_train 1y agoC++ is a good alternative to "C/C++"
- pjmlp 1y agoUnfortunely even big C++ powerhouses use plenty of C style programming on their pseudo-modern C++.
- crims0n 1y agoAlternatively, 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.
- School-Cotton 1y agoIt’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.
- echelon 1y agoGoogle 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.
- morshu9001 1y agoGo'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).
- zeroc8 1y agoJava's biggest problem is the fact that mutability is so baked into the language. I'm working on a project now where I always need to dig deep to find out if something has been mutated or not. Yes, there are records and we are now getting into data oriented programming. But older codebases are really hard to read.
- GreenWatermelon 1y ago
- ranger_danger 1y agoPersonally 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.
- aabhay 1y agoSwift, 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.
- morshu9001 1y agoSwift syntax did feel overly fancy to me too. Look at how complicated and version-dependent the StackOverflow Swift answers are for conceptually simple things.
- deleted 1y ago[deleted]
- markasoftware 1y agoTheir 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?
- forthac 1y agoThis was posted to about a day ago: https://github.com/johnperry-math/AoC2023/blob/master/More_Detailed_Comparison.md 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. By contrast, the Rust programs I've seen tend to specify types in terms of low-level, machine types. Thus, I tried to address the same problem using an f64. In this particular case, there were repercussions, but usually that works fine as long as you know what the machine types can do. You can index Rust types with non-integers, but it takes quite a bit more work than Ada. ```
- Pet_Ant 1y ago> By contrast, the Rust programs I've seen tend to specify types in terms of low-level, machine types. This seems to be an artifact of the domain that Rust is currently being used in. I don't think it's anathema to Rust to evolve to be able to add some of these features. char indexed arrays are something I've used a lot (most via `char c - 'a'`\, but native support for it would be nice).
- sgsjchs 1y agoYou very rarely would actually want scalar types which don't map directly to hardware supported ones anyway.
- m00dy 1y agoyes, you should.
- WalterBright 1y agoDlang is the GOAT!
- xedrac 1y agoHaha, Walter you're definitely not biased on this one. :)
- WalterBright 1y agoMe? Biased? LOL
- timeon 1y agoI think that was appropriate comment under article "Should I choose Ada?" posted on adacore dot com.
- SurajMishra 1y agoThe truth has been spoken.
- deleted 1y ago[deleted]
- alberth 1y agoSPARK is used by NVIDIA for the most secure compute code. https://www.adacore.com/nvidia https://www.adacore.com/nvidia
- EverydayBalloon 1y ago[dead]
- waterTanuki 1y ago> 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.
- ajxs 1y ago> 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_Against_Rust.html#buffer_overflow https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...
- vouwfietsman 1y agoI 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".
- drnick1 1y agoNo, just learn C/C++ properly.
- simonask 1y agoI've worked with some of the best C++ programmers on the planet, and none of them would ever propose this as a solution. They are the first to recognize that developing software in C++ is expensive and error-prone. We've tried this for decades.
- moi2388 1y agoHow does Ada/Spark compare to theorem provers like Agda and Lean, in terms of guarantees? I’m not really into languages like this. Anybody got some resources regarding how strict the guarantees can get in either of these types of environments?
- ramon156 1y agoThe average HN comment section has kind of become a new reddit and I'm kind of pessimistic about it. I see the same low effort comments lately, and I moved away from Reddit for that very reason. Maybe these type of questions just attract the same people.
- MichaelEstes 1y agoI might be in the minority, but I hate type re-definitions, I want types to just tell me how much memory a variable is using and it’s bit interpretation. Every variable already has a name, use that to communicate the data’s representation and if it’s really important that representation mismatches are caught at compile time wrap it in a struct. I don’t want to guess how much memory the compiler decided a variable needed (though that is also present to an extent in C/C++)
- nosianu 1y agoUnderstandable. Many many years ago I sat in front of a commercial code base for the very first time, a well-known large database company, and my first despair-level was reached quickly when I saw that everybody who ever submitted a patch seemed to have created their own version of very basic types such as 32 bit unsigned integers, making following the code and checking the types on the way very hard. On the other hand, these kinds of types for different kinds of numbers are meant for higher-level checks. Not confusing some random number with a monetary amount, or, as in the example, miles with kilometers, sure helps. The latter might have prevented that Mars mission that failed due to such a unit error (Mars Climate Orbiter). The problem, as so often, is that we only have one source code (level), but very different levels of abstraction. Similar when you try to add very low-level things like caching, that have to be concerned with implementation and hardware, and mix it with business logic (alternative: even more abstraction and code to try to separate the two, but then you will have more indirection and less knowledge of what is really going on when you need to debug something). Sometimes you are interested in the low-level concepts, such as number of bytes, but other types you want some higher level ideas expressed in your types. Yet, we only have one type layer and have to put it all in there, or choose only one and then the other kind of view suffers.
- rramadass 1y agoOne can learn to apply Formal Methods at many levels in any language using available tools at hand. For some ideas see; 1) On Formal Methods Thinking in Computer Science Education - https://dl.acm.org/doi/10.1145/3670419 https://dl.acm.org/doi/10.1145/3670419 2) (In-)Formal Methods: The Lost Art --- A Users’ Manual by Carroll Morgan - https://fme-teaching.github.io/2019/10/03/in-formal-methods-the-lost-art-a-users-manual/ https://fme-teaching.github.io/2019/10/03/in-formal-methods-... 3) Forthcoming book by Carroll Morgan Formal Methods, Informally How to Write Programs That Work - https://www.cambridge.org/highereducation/books/formal-methods-informally/4DE900050EB3C855E4BB627A94B4176E#overview https://www.cambridge.org/highereducation/books/formal-metho... 4) Understanding Formal Methods by Jean-Francois Monin - A firehose of information.
- deleted 1y ago[deleted]
- psyclobe 1y agoYou should choose c++ of course
- dmh2000 1y agoDo you want mainstream (rust) or relatively obscure (ada). Yes I know it's been around since 1980 when it was a cash grab for defense contractors.
- 1vuio0pswjnm7 1y agoAFAIK, the people behind the Rust compiler do not include anyone like the late Robert K Dewar I really like the other compilers he worked on, e.g., SPITBOL, SETL He taught CS but he studied chemistry as a student
- casey2 1y agoI remember hearing on a stream, and I find it to be true, that Rusts major innovation over Haskell, another boilerplate heavy language if your goal is systems programming, is that instead of "purity" which any sane programmer would just discard as useless right way they innovate "saftey" as a propaganda word, as a moral failing of the programmer for ignoring what is quite clearly useless.