Should I choose Ada, SPARK, or Rust over C/C++? (2024)
blog.adacore.com
blog.adacore.com
I don't know much about Ada. Is its type system any better than Rust's?
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.
```
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).
F'90 added arbitrary lower bounds on assumed-shape dummy arrays, as well as on allocatables and pointers. Still pretty portable, though more confusing cases were added. F'2003 then added automatic (re)allocation of allocatables, and the results continue to astonish users. And only two compilers get them right, so they're not portable, either.
Ada's array indexing is part of its type system. Fortran's is not (for variables).
It's just much, much easier and more ergonomic in Ada.
There was a header only library on the Windows SDK that would wrap those HANDLEs into more specific types, that would still be compatible, while providing a more high level API to use them from C.
Unfortunely there is not much left on the Internet about it, but this article provides some insight,
https://www.codeguru.com/windows/using-message-crackers-in-t...
Naturally it was saner just to use TP/C++ alongside OWL, C++ with MFC back then, or VB.
C++: That, but with a billion operator overloads and conversion operators so they feel just like native integers.
Of course you can use a unit type that handles conversions AND mathematical operations. Feet to meter cubed and you get m³, and the library will throw a compile error if you try to assign it to anything it doesn't work with (liters would be fine, for example)
News flash, C++ has every conceivable feature, it's the reason why it is so unwieldy. But you can even plug in a fucking GC if you so desire. Let alone stuff like basic meta programming.
> Feet to meter cubed and you get m³, and the library will throw a compile error if you try to assign it to anything it doesn't work with (liters would be fine, for example)
Liters would not be fine if you are using standard floating point values since you lose precision moving decimal points in some cases. Maybe for your application the values are such that this doesn't matter, but without understanding your problem in depth you cannot make the generic statement.
I could write books (I won't but I could) on all the compromises and trade offs in building a unit type library.
The 'explicit' would force you to use static_cast
And as usual, it mostly comes with zero overhead, beyond optional runtime range checking and unit conversions.
But C++ is a meta-programming language. Making up your own types with full operator overloading and implicit and explicit conversions is rather easy.
And the ADA feature of automatically selecting a suitable type under the hood isn't actually that useful, since computers don't really handle that many basic types on a hardware level. (And just to be clear, C++ templates can do the same either way)
In C++ operator overloading can easily mess with fundamental mechanisms, often intentionally; in Python it is usually no more dangerous than defining regular functions and usually employed purposefully for types that form nice algebraic structures.
class MyNum(int):
def __add__ (self, other):
return super().__add__(other) * 10
n = MyNum(12)
a = 45
print(n + a) # oops class MyNum(int):
def ten_times_sum (self, other):
return (self+other)* 10
n = MyNum(12)
a = 45
print(n.ten_times_sum(a))
Operator overload is indeed syntactic sugar for function calls, regardless of the language.
By the way, you can overload >> in Python via rshift(), or __rshift__() methods.
You mean accumulated prejudices, myths, and superstitions that most in any given community (programming language related or not) won't challenge for fear of being cast out of the group for heresy.
type Temperature_K is digits 6 range 0 .. <whatever is reasonable upper bound in your domain>;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.
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.
> ...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...
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".
Different type systems are capable of expressing different valid states with different levels of expressivity at compile time. Rust could originally express constraints that SPARK couldn't and vice-versa, and the two continue to gain new capabilities.
I think in this specific example it's possible to write a Rust program that can be (almost) verified at compile time, but doing so would be rather awkward in comparison (e.g., custom array type that implements Index for a custom bounded integer type, etc.). The main hole I can think of is the runtime check that the index is in bounds since that's not a first-class concept in the Rust type system. Easy to get right in this specific instance, but I could imagine potentially tripping up in more complex programs.
Yes, you could theoretically generate a Rust program that does not compile if some theorem does not hold, but this is often times (unless the theorem is about types) not a straightforward Rust program for the problem at hand.
I also think that, although Rust is blurring the lines a bit, equating formal verification and type-checking is not a valid stance. A type checker is a specific kind of formal verification that can operate on a program, but it will only ever verify a subset of all hypotheses: those about object types.
You're right. Validating input is a part of this process. The compiler can trivially disprove that the array can be safely indexed by the full set of any valid integer that the user can input. Adding a runtime check to ensure we have a valid index isn't a very impressive use of formal proofs, I admit. It's just a simple example that clearly demonstrates how SPARK can prove 'memory-safety' properties.
procedure Overflow_This_Buffer
with SPARK_Mode => On
is
type Integer_Array is array (Positive range <>) of Integer;
Int_Array : Integer_Array (1 .. 10) := [others => 1];
Index_To_Clear : Integer;
begin
Ada.Text_IO.Put ("What array index should be cleared? ");
-- Read the new array size from stdin.
Ada.Integer_Text_IO.Get (Index_To_Clear);
Int_Array (Index_To_Clear) := 0;
end Overflow_This_Buffer;
How did you prove that no one could just put in an arbitrary integer into that function? Does it fail to compile? Then you're just making a custom type which enforces valid state which, again can be done in any language with a rich type system and if statements.
If I might be more blunt: formal proofs in the field of programming appear to be nothing more than mathematicians trying to strong-arm their way into the industry where they aren't necessarily needed. Formal proofs make sense when you're trying to come up with new formulas or studying the cosmos, but they make no sense when you're trying to predict how bits will behave on a computer, because for the most part that is a solved problem by languages themselves.
The answer quite literally follows immediately after the code sample you quoted:
> Attempting to prove the absence of runtime errors gives us the following warnings:
buffer_overflow.adb:162:26: medium: unexpected exception might be raised
162 | Ada.Integer_Text_IO.Get (Index_To_Clear);
| ~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~
buffer_overflow.adb:164:18: medium: array index check might fail
164 | Int_Array (Index_To_Clear) := 0;
| ^~~~~~~~~~~~~~
reason for check: value must be a valid index into the array
possible fix: postcondition of call at line 162 should mention Item
(for argument Index_To_Clear)
162 | Ada.Integer_Text_IO.Get (Index_To_Clear);
| ^ here
This is followed by a version of the program which SPARK accepts.
> Then you're just making a custom type which enforces valid state which, again can be done in any language with a rich type system and if statements.
Key word here is can. You can write correct software using any language, from raw binary to theorem proving languages, but some languages check more properties at compile time than others. What using something like SPARK/Lean/Agda/Rocq buys you is the "more" part, up to allowing you to eliminate runtime checks entirely because you proved at compile time that the corresponding error conditions can not happen (e.g., proving that indices are always in bounds allows you to omit bounds checks). That's not something the more popular languages are capable of because their type system is not expressive enough.
> Formal proofs make sense when you're trying to come up with new formulas or studying the cosmos, but they make no sense when you're trying to predict how bits will behave on a computer, because for the most part that is a solved problem by languages themselves.
This seems contradictory, especially when considering that type checking is creating a formal proof?
To me, this doesn't sound like something unique to spark. Let's return to the solution example:
procedure Overflow_This_Buffer
with SPARK_Mode => On
is
type Integer_Array is array (Positive range <>) of Integer;
Int_Array : Integer_Array (1 .. 10) := [others => 1];
Index_To_Clear : Integer := Int_Array'First - 1;
begin
while Index_To_Clear not in Int_Array'Range loop
Ada.Text_IO.Put ("What array index should be cleared? ");
-- Read the new array size from stdin.
Ada.Integer_Text_IO.Get (Index_To_Clear);
end loop;
Int_Array (Index_To_Clear) := 0;
end Overflow_This_Buffer;
> If we wrap the Get call in a loop, and poll the user continuously until we have a value within the array bounds, SPARK can actually prove that a buffer overflow can't occur. (Remember to initialise the Index_To_Clear variable to something outside this range!)
You have to poll the user continuously until a valid input is given. Again, I don't see how this is any different or special compared to any other programming language that would handle the error by asking the user to retry the function.
> Key word here is can. You can write correct software using any language, from raw binary to theorem proving languages, but some languages check more properties at compile time than others. What using something like SPARK/Lean/Agda/Rocq buys you is the "more" part, up to allowing you to eliminate runtime checks entirely because you proved at compile time that the corresponding error conditions can not happen (e.g., proving that indices are always in bounds allows you to omit bounds checks). That's not something the more popular languages are capable of because their type system is not expressive enough.
But I think the discussion here is about Rust, Ada, C/C++ no? The type system in Rust, Ada, and C++ are all robust enough at least to accomplish this.
> This seems contradictory, especially when considering that type checking is creating a formal proof?
Exactly! This is the root of my issue: you can accomplish this magical "proof" you speak of without using SPARK or Ada or any special "contract" language.
The blog's emphasis is that SPARK catches the possible error at compile time, so you can't forget/neglect to handle the error. Notice that neither rustc nor clippy complain at compile time about the potential OOB access in the Rust program that precedes the SPARK demo, while SPARK catches the potential issue in the naive translation.
> But I think the discussion here is about Rust, Ada, C/C++ no?
Sure, but my point is that type systems are not all equally capable. I don't think it's controversial at all that Rust's type system is capable of proving things at compile time that C++'s type system cannot, the most obvious examples being memory safety and data race safety. Likewise, SPARK (and C++, for that matter) is capable of things that Rust is not.
> The type system in Rust, Ada, and C++ are all robust enough at least to accomplish this.
I'm not sure about that? You might be able to approach what SPARK could do, but at least off the top of my head you'll need to make a check the compiler can't verify somewhere.
And that's just for this instance; I don't think Rust nor C++ are able to match SPARK's more general capabilities. For example, I believe neither Rust nor C++ are able to express "this will not panic/throw" in their type systems. There are tricks for the former that approximate the functionality (e.g., dtolnay/no_panic [0]), but those are not part of the type system and have limitations (e.g., does not work with panic=abort). The latter has `noexcept`, but that's basically semantically a try { } catch (...) { std::terminate(); } around the corresponding function and it certainly won't stop you from throwing or calling a throwing function anyways.
> Exactly! This is the root of my issue: you can accomplish this magical "proof" you speak of without using SPARK or Ada or any special "contract" language.
Perhaps I wasn't clear enough. I was trying to say that it's contradictory to complain about formal proofs while also claiming you can accomplish the same using other programming languages' type systems because those type systems are formal proofs! It's like saying "You don't need formal proofs; just use this other kind of formal proofs".
I don't think that assertion is correct either. The reason separate languages are used for this kind of proof is because they restrict operations that can't be proven, add constructs that provide additional information needed for the proof, or both. Perhaps as an extreme example, consider trying to make compile-time proofs for a "traditional" dynamically-typed language - Smalltalk, pre-type-hints Python, Lua, etc.
The idea is that you define a number of pre- and post- condition predicates for a function that you want proved (in what's effectively the header file of your Ada program). Like with tests, these checks that show that the output is correct are often shorter than the function body, as in this sorting example.
Then you implement your function body and the prover attempts to verify that your post-conditions hold given the pre-conditions. Along the way it tries to check other stuff like overflows, whether the pre- and post- conditions of the routines called inside are satisfied, etc. So you can use the prover to try to ensure in compile-time that any properties that you care about in your program are satisfied that you may otherwise catch in run-time via assertions.
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.
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.
How does that work out? Does he never uses arrays and strings?
array[expression]
if "array" has a bound whatever expression evaluates to can be checked against the bound of array. If "array" is not a bounded array but a pointer or an unbounded array, then this does not work, but my point is that it is easy to avoid such code.
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.
Which languages remove which classes of bugs entirely? This vagueness is killing me
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.
Pretty much every language has such a subset. Nothing new then, sigh...
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.
Taking this default is not enough to write safety-critical software… but it’s enough to write a browser (in theory) or some Android core daemons.
I can see how this would be confusing and probably should have been clarified with emphasis in the original comment. Safety in the sense of "safety critical" isn't a property any programming language can have on its own, so I wouldn't have intended that regardless.
[0] https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html
Sure, a segfault could potentially make some device fail to do its safety critical operation, but that is treated in the same way a logic bug would be, so it's not really a concern in of itself.
But then again, an unchecked .unwrap() would lead to the same failure mode, so a "safe" crash just just as bad as an "unsafe" one.
For example, lifetimes are necessary for memory safety in Rust, but you can use lifetimes much more generally to express things like "while this object exists, this other object is inaccessible", or "this thing is strictly read-only under these particular conditions". That's very useful.
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.
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.
Continuity: Ada is not widely taught at universities, and, whilst the AdaCore’s GNAT Academic Program (GAP) does exist, one has to consciously seek out a university that offers a course in/on Ada. Ada and programming in Ada is not common knowledge, which stems from the next point.
PR. Ada, rightfully or wrongully, does not exactly bask in the limelight of popularity – most assuredly not to the same extent as Python, NodeJs, Typescript, C#/.NET etc do. The current generation of Ada developers do not care (and probably should not), and the young and future generations of potential Ada developers miss out. Ada is not talked about in diverse contexts spanning web development, frontend/backend[0] development, containers, cloud – and the list goes on. Not because Ada can't be used in any of the aforementioned contexts, it is just that due to the lack of PR it remains an unnoticed reality – kind of like «if a tree falls in a forest and no one is around to hear it, does it make a sound?»
[0] Yes, «frontend development» and «backend development» are the fancy terms in wide use that the new generation can easily understand.
Sadly, Mathworks have monopoly there.
Also in safety critical apps, being "difficult" can be a feature, not a big. Should we have easier turbofans so we can pop them open and swap out blades and rings for tiny little improvements? No. Every flight critical component should be fully understood as a prerequisite for use.
Are you under the impression that software for aircraft is exceptionally good? A lot of the software for aircraft (for LRUs, avionics, whatever) are made by the same kind of developers as most other software.
1) On Formal Methods Thinking in Computer Science Education - 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-...
3) Forthcoming book by Carroll Morgan Formal Methods, Informally How to Write Programs That Work - https://www.cambridge.org/highereducation/books/formal-metho...
4) Understanding Formal Methods by Jean-Francois Monin - A firehose of information.
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.
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
And yes you’re right, it’s a very good language.
Yet another provable code I have found in Eiffel. There is "proven" doubly linked list in Eiffel. Something not possible in SPARK, going against unique pointers. Something not possible in Lean, going against immutability.
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?
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.
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.
I really like the other compilers he worked on, e.g., SPITBOL, SETL
He taught CS but he studied chemistry as a student
We've tried this for decades.
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.
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).
It's like a JRPG that may be a slog at the beginning, but then really gets going after the first 50-60 hours. Just gotta replace the hours with years, and huff even more glue.
And these are the people moaning about Rust and religious thinking... good old DARVO at it again, and it's growing more and more on the nose.