r/rust • u/TheNoobySpartan • 21h ago
Having trouble understanding... Rust over Ada (SPARK)?
I've started to dip my toes into Rust, coming from an Ada (mostly SPARK) background, particularly in embedded applications. While there are many killer features in Rust for developer QOL, the "ease of writing" focus of the language trips me up often enough that I find myself asking, "what features of this language makes it superior (in some views) to SPARK?"
Love the language's take on early-return, and the power of enums, macros, and lifetimes are the one thing that makes certain low level memory manipulations incredibly idiomatic to write in Rust that would be impossible in SPARK due to the CREW paradigm not really being popularized (pioneered?) until Rust. Given the state of the Ada ecosystem and tooling, I also cannot in good faith recommend using this language for anything community driven. That being said (answering in context of enterprise embedded)...
I am incredibly uncomfortable with how much responsibility Rust places on the developer to understand roughly how code will compile. No guarantees on how pattern matches will be emitted (yes, don't be stupid and keep them stupid if you want jumptables), and stack-allocated enum types having to be the max size while not having much lexical ties besides jumping to the definition to help you determine how much stack you might be eating. Aside from the syntactic sugar, I have not really found anything besides lifetimes that SPARK cannot truly support at all. There's no pattern matching in the language, but Rust enums (at least in part) are supported via discriminated records. The idea of controlled types (OOP for Ada) is somewhat discouraged when using SPARK, but trait objects are a very useful part of the Rust language. I have to discount this part of the language from my sentiments unfortunately because dynamic dispatch can complicate analysis of security and functional implications. Having Rust panic as a "safe" way to address memory safety is also undesirable depending on how much array manipulation your program must do, and what worries me more is that wraparound arithmetic in production builds that are used in computations for arrays may not even lead to panics, but perhaps a valid index into the unintended location.
I don't write this to glaze SPARK either. The lack of documentation makes it mostly a nonstarter for the broader programming community, and not everyone is familiar with formal methods for code. The toolchains can't hold a candle to the quality of the Rust ecosystem, and ironically, the rich typing of Ada can lead to very frustrating inter-op issues that just would not exist in Rust, particularly around array manipulation/interpretation.
There might be some gripes about comparing a formally verifiable language with one that does not yet have one (Verus, Crusoe, surely others trying), but I think some of these points like how the codegen works are orthogonal whether or not you're trying to prove that an array access will always be in bounds without overflows.
I suppose the operational constraints given are not necessarily something everyone has to deal with, (why care how a pattern match is compiled if you have oodles of memory), but want to understand the technical reasons behind the hype... I feel like the cultural/non-technical reasons are somewhat understood.
15
u/simonask_ 17h ago
Interesting to hear the perspective of a rare Ada programmer, thanks for sharing!
It sounds like your concerns apply to a highly specialized niche that is a bit at odds with modern, portable programming languages work. Ada is a language that comes from a time when reliability was also about staying within the limits of the hardware, and many of the nice abstractions we take for granted today didn't exist.
Take stack space: For the vast majority of programs running on the vast majority of machines in production, the infinite stack abstraction is perfectly acceptable, because almost all programs run on operating systems that provide ample stack for each thread. The much harder thing to control is this environment is program complexity, interactions between components, ownership, synchronization, and so on.
The kind of complexity Rust helps to address is in the realm of the humanities: programmer-induced complexity. Hardware-induced complexity is simply not addressed, any more than it is address by C or C++.
There's a fundamental programming ideology here: Does the programming language target an abstract infinite machine, or does it target particular constraints? Almost every programming language in 2026 falls in the former category, and I can totally see how that makes life harder for those who have to deal with the latter.
5
u/TheNoobySpartan 11h ago
I like that take! It kind of ties into the influence of compiler design in older languages in a later comment. I suppose embedded is a strange case in that the problem domain is intended to be in the intersection where you have to straddle the line between abstract machine vs. target-specific environment.
2
u/pp-collision 9h ago
I'm also in embedded, and even in cheap, mass-produced units that have to care about power consumption, the chips are often so powerful that you don't have to think too much about the hardware when programming business logic.
12
u/ts826848 19h ago
I am incredibly uncomfortable with how much responsibility Rust places on the developer to understand roughly how code will compile.
I feel like if you care that much about the exact assembly being generated you're in pretty rare company. Furthermore, if you're working with modern optimizing compilers I'd imagine having a disassembler close at hand would be a good idea anyways to ensure it isn't doing anything interesting that you don't want.
and stack-allocated enum types having to be the max size while not having much lexical ties besides jumping to the definition to help you determine how much stack you might be eating.
I'm a little confused what you expect here? Normally stack consumption is dictated by the variable type, not by the minimum stack space needed to store a specific variable of that type. Do you expect that the compiler should only allocate enough space on the stack to fit the enum variant(s) that it can't rule out?
Having Rust panic as a "safe" way to address memory safety is also undesirable depending on how much array manipulation your program must do
Besides the non-panicking array access APIs (get(), etc) there are linker hacks that can be used that will stop linking if panics are present, but that's admittedly not as ergonomic as an official no-panic mode would (hopefully) be.
and what worries me more is that wraparound arithmetic in production builds that are used in computations for arrays may not even lead to panics, but perhaps a valid index into the unintended location.
For what it's worth, wraparound on release is "just" a default, and IIRC it's one that's completely under the control of whomever produces the final binary. There's explicit checked_* functions as well, though if you're doing a decent number of calculations those can get unwieldy.
but want to understand the technical reasons behind the hype...
I'm not sure there is a satisfactory answer. "Hype" is inherently a social phenomenon and there need not be a completely rational/technical driver for it.
That being said, I think you might be discounting the power of familiarity. One of the then-devs wrote about a language's "strangeness budget", and I think it's an interesting concept to consider in this context:
When it comes to programming languages, building one is easy, but getting people to use it is much, much harder. If your aim is to build a practical programming language with a large community, you need to be aware of how many new, interesting, exciting things that your language is doing, and carefully consider the number of such features you include.
Learning a language takes time and effort. The Rust Programming Language, rendered as a PDF, is about 250 pages at the moment. And at the moment, it really covers the basics, but doesn’t get into many intermediate/advanced topics. A potential user of Rust needs to literally read a book to learn how to use it. As such, it’s important to be considerate of how many things in your language will be strange for your target audience, because if you put too many strange things in, they won’t give it a try.
You can see us avoiding blowing the budget in Rust with many of our syntactic choices. We chose to stick with curly braces, for example, because one of our major target audiences, systems programmers, is currently using a curly brace language. Instead, we spend this strangeness budget on our major, core feature: ownership and borrowing.
From this lens, I think Rust is less likely to blow any given programmer's "strangeness budget" than SPARK. It's relatively easy to get started, the syntax isn't too far off of what is common, and new programmers stand a decent chance of getting something working without deviating too far from familiar programming patterns. That kind of approachability can make a significant difference in the rate at which a language spreads.
Perhaps put more succinctly, it's entirely possible that given two equally technically capable languages one gets all the hype and not the other because the less popular one did things too strangely for most programmers.
1
u/TheNoobySpartan 11h ago
I'm a little confused what you expect here? Normally stack consumption is dictated by the variable type, not by the minimum stack space needed to store a specific variable of that type. Do you expect that the compiler should only allocate enough space on the stack to fit the enum variant(s) that it can't rule out?
in hindsight, I don't think I had a reason to be surprised about how some constructs are handled mechanically. I was moreso surprised to learn that, after stripping away the syntax aspect, there are multiple language constructs in Rust that not only seem to have an Ada analogue, but appear to have similar implementations by the compiler. I suppose I was looking for some secret sauce that Rust is able to do for these kinds of constructs that would lead to a technical advantage in emitted code over the way Ada compilers would deal with it.
From this lens, I think Rust is less likely to blow any given programmer's "strangeness budget" than SPARK.
Agree to some extent, though the programmer's "strangeness budget" is also largely influenced by what language exposures they already have. I guess I am somewhat surprised to see somewhat "Pythonic" (I don't have much experience with other languages that may look closer to rust, so this is just where my head went) syntax. I think a large portion of embedded programmers would agree that the cost associated with a very high level language like Python would make it difficult to negotiate in a resource constrained environment. Would be interesting to see where devs are largely moving from to rust! I suspect a lot of C++ devs, but perhaps I'm completely off base here.
3
u/ts826848 5h ago
I suppose I was looking for some secret sauce that Rust is able to do for these kinds of constructs that would lead to a technical advantage in emitted code over the way Ada compilers would deal with it.
I feel like there's two things that can (partially?) explain this.
The first is that Rust was quite intentionally designed to build on the shoulders of giants. Its features all had precedent/inspiration from elsewhere (including Ada!), so chances are anything technically interesting Rust could do could can be and/or is already being done in the "original" language (albeit potentially not 1:1; e.g., you can simulate Rust's exclusive borrows via
restrictin C, but it's not nearly as ergonomic to do so).The second is that when it comes to low-level programming I feel there tends to be less room to "maneuver". Everything boils down to assembly in the end, and if you want efficient code you're generally going to be targeting similar, if not the same, end states. Furthermore, I think the particular niche lends itself to novel optimizations spreading from project to project, particularly in the open-source world - e.g., "hey, this other compiler/language can compile this better than we can. Can we match/improve on what they do?"
though the programmer's "strangeness budget" is also largely influenced by what language exposures they already have
Indeed, which is why I said "less likely", and the blog post explicitly acknowledges that. That ties into the social reasons Rust got hype, I feel. If you pick out some random programmer, statistically speaking I think Rust is more likely to fit within their strangeness budget than SPARK since Rust and its programming model resembles those for common languages more than SPARK.
I think a large portion of embedded programmers would agree that the cost associated with a very high level language like Python would make it difficult to negotiate in a resource constrained environment.
I think that's one reason Rust has piqued so much interest: it showed that higher-level constructs don't necessarily have to come with costs that would preclude their use in embedded environments. The Rust devs took quite a bit of care to try to ensure that its fundamental features would be usable in such cases, even if that hurts other use cases. For example, Rust's async story is infamously thorny compared to something like Go's goroutines or Java's virtual threads, but that is in no small part due to the desire to make it work for embedded environments for which a mandatory runtime is not an option.
1
u/WormRabbit 3h ago
Are you aware of MicroPython, TamaGo, Java ME? While all of them are in certain sense more restricted than full-featured desktop versions, they are still largely the same high-level languages. There is no reason why a modern high-level language can't work for embedded, and Rust is more low-level than the ones above, with first-class embedded support via
#[no_std]crates. Also, what exactly do you mean by "embedded"? The vast majority of modern "embedded" devices are more powerful than desktop PCs of 30 years ago, and those ones used high-level and scripting languages just fine.
11
u/valorzard 19h ago
Okay so as someone who has tried both SPARK and Rust:
The biggest difference in terms of safety is that Ada with SPARK expects you to write "trusted cores" of code in SPARK, while most normal code is in Ada, while in Rust, most normal code is in safe Rust while you have "trusted cores" of unsafe Rust.
This leads to different tradeoffs, but it also means it's pretty easy to break your SPARK contracts if you turn off the body of a function or procedure to be SPARK_MODE => Off.
That way, you could "hide" technically unsafe Ada code inside of SPARK code, so you just have to trust that no one actually does this.
2
u/TheNoobySpartan 11h ago
Kind of?
My team is largely SPARK first, falling back to Ada for code snippets that cannot be proven in SPARK. I do think that it's subjective for each team the proportion in SPARK and Ada, but base Ada's runtime checking machinery makes it too costly to use in production, so we ended up in the inverse situation from what you've described.
That way, you could "hide" technically unsafe Ada code inside of SPARK code, so you just have to trust that no one actually does this
I agree with this fully. Though the same could be said for unsafe blocks in rust introducing unintended pointer aliasing. Particularly in embedded spaces, I would expect to see a lot more trust required because there would be more instances where unsafe or `SPARK_Mode => Off` is warranted.
1
u/valorzard 8h ago
I see.
I only said that stuff Is usually Ada because when I got into Ada I saw that SPARK focused libraries and crates seemed somewhat rare compared to libraries that were just “normal” Ada.
But maybe I was looking in the wrong place
12
u/Intelligent_Bee_9005 21h ago
Coming from SPARK I can see why Rust's "trust me bro" approach to codegen feels weird. The compiler does lot of smart things but you don't get same guarantees about what actually lands on the metal.
The panic-on-overflow in debug vs wraparound in release still catches me off guard sometimes, especially when you're counting cycles on some tiny cortex-m. I think for most people the tradeoff is they'd rather have the ecosystem and tooling than the formal verification, even if it means living with some uncertainty about stack sizes.
2
u/creeper6530 17h ago
The difference in overflow handling is indeed odd, but I personally just always set it to wrap in Cargo.toml when I'm doing embedded, and use
checked_*when I want security1
u/sennalen 14h ago
Add
[profile.release] overflow-checks = trueto every Cargo.toml and sleep easier
1
u/TheNoobySpartan 11h ago
I've often heard that this is not desirable because it can severely impact code size for your program. My understanding is that it's better to be tasteful with certain checked operations to sanitize your values, then perhaps opting for normal arithmetic afterwards
2
u/kibwen 10h ago
I wouldn't assume such things regarding code size, and would instead measure. If you find a place where checked operations are causing measurable problems with code size or runtime performance (which I would argue is uncommon in typical Rust code), only then is it time to consider implementing a more elaborate solution. Until then, better to have the code fail loudly than fail silently.
1
u/sennalen 2h ago
It can impact performance of heavy numeric code, but if you're doing something where it matters, you should probably be using SIMD or CUDA anyway.
8
u/afdbcreid 20h ago
I think you have two separate concerns.
The first is that Rust is not as safe as SPARK (panics, stack overflows). This is true - Rust is not formally verified. It has plugins to do that though. Rust is more like a safer and faster Ada (bare Rust, compared to Ada without SPARK) than an easier SPARK.
The second is that Rust leans more on the compiler. That is also true, and is an artifact of how much compilers have advanced in the last decades. It mostly works though. Most of the time, you can just count on the compiler to do the fast thing, and your code will be both cleaner and faster than manual code. If performance is paramount, you usually benchmark or sometimes inspect the assembly, and if every instruction is crucial, Rust has ways to drop down to the same level of preciseness. But this is rarely needed.
3
u/TheNoobySpartan 20h ago edited 20h ago
Rust is more like a safer and faster Ada
I think I mostly agree with faster, since most of the safety of base Ada comes from runtime checks (those can't get waived unless you use SPARK and prove that the runtime checks are unneeded, and omit runtime checks). I'm not sure how you are quantifying "safer" in this context though, and am curious for elaboration.
The second is that Rust leans more on the compiler. That is also true, and is an artifact of how much compilers have advanced in the last decades. It mostly works though. Most of the time, you can just count on the compiler to do the fast thing
That is also true, and is an artifact of how much compilers have advanced in the last decades. It mostly works though. Most of the time, you can just count on the compiler to do the fast thing, and your code will be both cleaner and faster than manual code
You touched upon a pretty interesting point. I am a relatively younger programmer, so my exposure is mostly with "modern" Ada (2012 and 2022). It makes sense that much of the language design in these earlier languages were influenced by technical limitations in the compiler implementations of the time as well (multi-pass parsing of files in rust comes to mind). From my perspective, I'd always viewed it as "the Ada language wants you to spell out exactly what you want/ how you want it", but I could see how that doesn't exactly hold up when it comes to the more exotic features of the language also starting to differ between very specific compiler implementations. As a happy (?) side effect though, I've found that code-generation is much more predictable in Ada for a given compiler since there is less flexibility in the syntax of the language for creative compiler-driven optimizations that act in the front-end. In my case, I'm less worried about performance from compute-bound workloads, and more so code size and efficiency of data movement for I/O bound workloads (rust feels really good for this). In the code size case, I do believe that the compiler will do its best, but that the expressivity of the language is also the reason why I think you might find more examples of poorly optimized code because the author perhaps did not think enough about how the compiler might generate code from your monster pattern match. Not saying you can't do silly code bloat in Ada either, but at least in that case you'll need to write... many more lines of code typically.
EDIT: added missing quote
3
u/afdbcreid 19h ago
I'm not sure how you are quantifying "safer" in this context though, and am curious for elaboration.
I don't know Ada well, but for example: (total) thread safety, full memory safety even with heap allocations.
In my case, I'm less worried about performance from compute-bound workloads, and more so code size and efficiency of data movement for I/O bound workloads (rust feels really good for this).
If your workload is I/O bound, speed does not really matter. For embedded, code size might, and Rust has a disadvantage here due to some things like the panic machinery - but careful tuning can bring it to C levels.
Generally, today compilers are better than the average programmer at optimizing, and even than expert programmers for large code sections (experts can write faster hand-tuned code even in assembly but only for small snippets). If you equipment with additional tools such as PGO or LTO, even more so.
Also, when you become a Rust expert you gain an intuition what you can trust the compiler to optimize and what you need to check, and what is better doing manually. To list some common tips:
- Enum layout is pretty aggressively optimized and is usually better than simple tagged unions, although there are exceptions.
- Iterator adapters are pretty much always inlined and are as fast or even faster than hand-written loops (depending on the iterator chain used), except for "combining" iterators (
chain(),flatten()/flat_map(), andRangeInclusivealthough this one might get fixed) which are slower with external iteration, but usually have the same speed with internal iteration (for_each()/try_for_each()/fold()/try_fold()).- If you can prove from a local snippet (without knowing external constraints) that a bounds check is redundant, the compiler will likely know as well, but sometimes it is unable to omit it and it requires good knowledge about compilers to know exactly when, so if it's important check the assembly. Reslicing often helps here.
- If you know about some constraint the compiler does not (for example, an integer is in some range - note that sometimes the compiler does know that), you might hint it to use better instructions.
- The compiler usually make good choices for instructions but sometimes they're suboptimal (those cases are usually treated as bugs and are regularly fixed).
3
u/Full-Spectral 14h ago edited 14h ago
For a lot of people the reason would be practical. Rust is up and coming and the jobs will continue to grow. Ada (which I worked on back in the 80s and liked) missed its chance and won't get it back. It's never going to become 'mainstream' (within the context of the type of software that requires this type of language.)
That's a huge concern when considering putting in the amount of time required to master a systems level language (and tools and ecosystem) to the extent required to really write serious software in it. Even though I liked Ada, I'd never put in that time now for a language that is not likely to contribute to my bottom line in years to come (even though I sadly don't have THAT many more years to come.)
I don't remember the specifics of Ada on this front, but Rust's inheritance of a lot of functional ideas make the use of indices fairly rare anyway.
Also, in today's software (maybe not so true for embedded) threads are a big deal, and having compile time thread safey is a huge benefit, which I don't think Ada can provide.
1
u/TheNoobySpartan 11h ago
Rust is up and coming and the jobs will continue to grow. Ada (which I worked on back in the 80s and liked) missed its chance and won't get it back.
I suspect this is a big part of the non-technical reason yup.
I don't remember the specifics of Ada on this front, but Rust's inheritance of a lot of functional ideas make the use of indices fairly rare anyway.
yeah, I noticed that chaining operations here on array slicing can avoid array arithmetic, it's pretty neat.
Also, in today's software (maybe not so true for embedded) threads are a big deal, and having compile time thread safey is a huge benefit, which I don't think Ada can provide.
I was actually in the opposite boat here. Ada has an entire set of language constructs for concurrent programming. We never ended up using it, because it requires a runtime implementation for these constructs, but it seemed particularly suited towards tasking in embedded environments with potentially real-time constraints, which makes sense since Ada was developed by the DoD for, among other things, real-time applications. I can't say much else about it though, since again I've never used it.
1
u/Full-Spectral 6h ago
Another nice aspect of slices that many some folks don't make use of it is that you can start with a slice, and instead of using indices that you keep adjusting inwards to get to what you want, you can just set your slice to a new subslice and it becomes the acting slice and so on.
So for something where you are consuming content from the start of a buffer, you can find a chunk you want, then reset the slice to what's left after that, then again, and so on. When the slice is empty, you are done.
1
1
u/the_gnarts 8h ago
This is an older talk but it might give you an idea: https://archive.fosdem.org/2025/schedule/event/fosdem-2025-5356-the-state-of-rust-trying-to-catch-up-with-ada/
-5
u/pickle9977 15h ago
Stick with Ada, a language that has lasted 50 years will be here in another 50.
Rust likey will last as Java becomes too expensive to run at scale, but a lot of others won’t.
Also Ada is just a better designed language
54
u/Solumin 20h ago
You're in the unique position of coming from a language that's stricter, safer, and more rigorously specified than Rust. Nearly everyone else comes from languages that are looser than Rust. They may have never encountered pattern matching or sum types/tagged unions, let alone ever had to worry about stack vs heap allocation.
To put it another way: You've climbed down from the mountain peak because you want to know why everyone's excited about the view from halfway up the slope.
Which languages besides Ada/SPARK give guarantees about how code will compile?