This is the original announcement from 2020,
"SPARK/Ada Journey to Adoption"
https://youtu.be/DZSSyWlsb28?si=vh4gO-LT2N3Skaql
Also we are now on Ada 202x already, quite different from Ada83, that some Rust folks keep comparing their favourite language with.
You get all the niceties of a language more in line with Object Pascal productivity, formal proofs, a RAII approach safer than C++ (controlled types, automatic stack types, unbound collection types), industry baremetal profiles like Ravenscar, and the recent versions are in the process of having affine types as well (aka borrow checker).
For example, it seems it's not possible to get a sub-string slice reference to an original unbounded string. In rust, a &str -> &str signature is trivial.
So it seems Ada still relies on discipline, while SPARK does not have the zero-cost abstractions that C++ and Rust have.
If that's true (is it?), then I'd definitely choose C++/Rust over Ada any time, since performance is very important to me.
Ada has as much zero cost abstractions as C++ and Rust have, and one of the reasons of Ravenscar is even what to turn off for bare metal deployments, and real time OS deployments.
> Ada has as much zero cost abstractions as C++ and Rust have.
Couldn't find anything about it (see above), but does Ada come with any monomorphization tricks?
The way generics are implemented in Ada compilers is implementation specific.
> What you don’t use, you don’t pay for. And further: What you do use, you couldn’t hand code any better.
without monomorphizing the generics?
Also I find funny this point of view on Ada, given the poor examples WG21 has added into the C++ standard library, that will never be fixed due to never-ending ABI drama.
With that said. How does:
> By letting the compilers decide the best way to implement them.
Get you to zero cost generics. What if implementor just says "let them eat memory" and boxes the generic.
Spark is a different use case from rust - it’s a full prover, and the goal is formal verification, typically in contexts where human life is at stake ( say, you’re writing software for an artificial heart , to take an extreme example ). This comes at the cost of being less flexible, but they’ve been slowly evolving spark so that it can handle increasingly complex cases .
Ada has had shared aliases since 1995. Its had zero cost abstractions since before then.
Slicing memory from a string is in the intro manual, for example.
my_var(2 .. 6)
Ada doesn't rely on you to be disciplined. [0] Memory safety comes with SPARK. Its a theorum prover.[0] https://blog.adacore.com/memory-safety-in-ada-and-spark-thro...
I think the closest thing to a &str in Ada would be an "access String" or "access constant String", which you would get either from an allocated "String" or from a declared "aliased String". You'd create a subslice with "string(x..y)'Access". Though I'm not sure whether that actually works without explicitly declaring an array of "aliased Character", the Manual is dense (as with C++, it's nearly meaningless unless you already know what it's supposed to mean) and the tutorials generally avoid talking about access objects.
To be more specific, how would one implement something like a "Get_First_Word" or "Trim_Whitespace" without copying?
[0] https://www.adaic.org/resources/add_content/docs/craft/html/...
[1] http://www.ada-auth.org/standards/22rm/html/RM-3-10-2.html
If you want a copy, with Unbounded String, you'll need to call To_String on the slice.
[0] https://sites.radford.edu/~nokie/classes/320/std_lib_html/ad...
Also, the Unbounded_String owns its copy of the data, as opposed to referencing other data. The difference with String seems to be just that it can grow. It's still more like std::string than std::string_view.
Note that both std::string and std::string_view are essentially just a pointer and a length (std::string also has a capacity but let's ignore that). The difference is that trying to duplicate a std::string will end up duplicating (deep-copying) the data behind the pointer as well, where as duplicating a std::string_view will not.
Could you help me understand/interpret that link the same way you do, in case I'm missing something?
But what Unbounded does is... "U.Reference (U.First .. U.Last)". It returns a reference. It's not duplicating, because that would defeat the point of its entire existence. Its the buffer, containing one or more string objects, and you're just slicing a reference out of it - because that's the point.
If you want a String, you need to allocate one.
function Slice
(Source : in Unbounded_String;
Low : in Positive;
High : in Natural)
return String;
For this - there is no `out` marked. What you're grabbing is part of Unbounded, and the compiler won't let you deallocate it. Because it's owned, as a reference, to the Unbounded String.For example, here's the actual GNAT source of the function [1]:
function Slice
(Source : Unbounded_String;
Low : Positive;
High : Natural) return String
is
begin
-- Note: test of High > Length is in accordance with AI95-00128
if Low - 1 > Source.Last or else High > Source.Last then
raise Index_Error;
else
return Source.Reference (Low .. High);
end if;
end Slice;
A pre-existing reference is returned. There is no allocation that happens whatsoever.[1] https://github.com/gcc-mirror/gcc/blob/master/gcc/ada/libgna...
It's really difficult to understand this given how much I know about Ada, so the best I can do is to keep throwing questions at ChatGPT. And I keep getting results that go against what you said.
I've also tried a couple direct review examples from o4-mini-high, one without the documentation link [1] and one with it [2].
It matches what I've managed to learn as well. I know how LLMs work and that they hallucinate a lot, so I can't tell who here is wrong, since you seem to be really experienced, and I barely know anything... what are your thoughts?
Oh, and I really appreciate you walking me though this! Like, a lot a lot! Thank you very much!
[1] https://chatgpt.com/share/684341e3-8e20-8012-b8d0-9847742af9...
[2] https://chatgpt.com/share/68434538-fe24-8012-bdb7-b07db34371...
If you're throwing something to a con-artist, don't be surprised if everything you get back does not line up with reality.
EDIT:
Here's a simple example on godbolt: https://godbolt.org/z/hcxhvGnTc
As you can see, it just returns a pointer. No copying happens. There's a different length marked along with the pointer, but that's it.
Looking at your Godbolt example's assembly, even if I add -O3, I see it does a call to "ada__strings__unbounded__unbounded_slice", but until I know the contents of that I can't say whether the pointer it returns is derived from the same allocation as the original one, or from a new allocation that the string was copied to.
You're using the Unbounded_Slice function [1], which calls To_Unbounded_String [2], which calls `new String` [3], which you mentioned in a previous comment that it will allocate, right?
The kind of operation I'm looking for is something like a "Trim_Whitespace" function that re-uses the old allocation without copying all the data, even when there is whitespace to trim.
[1] https://github.com/gcc-mirror/gcc/blob/master/gcc/ada/libgna...
[2] https://github.com/gcc-mirror/gcc/blob/master/gcc/ada/libgna...
[3] https://github.com/gcc-mirror/gcc/blob/master/gcc/ada/libgna...
You need a slice, which has a different length. That is how you do it, without a new allocation.
It's effectively:
struct String {
size_t length;
char\* buffer
};
struct String\* Unbounded_Slice(struct String\* original, size_t Low, size_t High) {
struct String\* slice = malloc(sizeof(struct String));
// Bounds checking would go here...
slice->buffer = original + Low;
slice->length = High;
return slice;
}
(The exact definition of a string is implementation-defined. But that's the concept.)Ada enforces safe ranges, which means you need to carry the length of the slice somehow. It does not use C's 0-terminated strings. So slicing does not work the same way as strtok or other self-modifying systems - the length isn't guessed, it's known.
But if you change one character in the buffer of the slice, it'll be changed in the original Unbounded_String too.
For trimming whitespace, you're right that Unbounded's standard Trim may reallocate. It carries multiple buffers, and when you Trim sometimes it will just hand it back, other times it'll reallocate. [0] Mostly for performance tradeoff. Keeping the original can make iteration slower, as it holds multiple buffers.
So, to implement our own - with one caveat. Slice can't handle 0-length, because range safety is enforced. So in the case of a wholly whitespace string, we'll be doing a whole new allocation.
-- This line is just for pasting into godbolt
pragma Source_File_Name (NTrim, Body_File_Name => "example.adb");
with Ada.Strings.Unbounded;
with Ada.Strings.Maps;
use Ada.Strings.Unbounded;
function NTrim(Source : Unbounded_String) return Unbounded_String is
Len : constant Natural := Length(Source);
First, Last : Natural;
Whitespace : constant Ada.Strings.Maps.Character_Set := Ada.Strings.Maps.To_Set(" " & ASCII.HT & ASCII.LF & ASCII.CR);
begin
if Len = 0 then
return Source;
end if;
First := 1;
while First <= Len and then Ada.Strings.Maps.Is_In(Element(Source, First), Whitespace) loop
First := First + 1;
end loop;
Last := Len;
while Last >= First and then Ada.Strings.Maps.Is_In(Element(Source, Last), Whitespace) loop
Last := Last - 1;
end loop;
if First > Last then
return To_Unbounded_String("");
end if;
declare
Trimmed_Length : constant Natural := Last - First + 1;
begin
if Trimmed_Length >= 3 then
return Unbounded_Slice(Source, First, First + 2);
else
return Unbounded_Slice(Source, First, Last);
end if;
end;
end NTrim;
The resulting compilation [1] has a few things. Our whitespace map gets allocated and deallocated most of the time. A map is harder to treat as a constant, and the compiler doesn't always optimise that nicely. Most of the code is bounds checking. No off-by-one allowed, here. Where first is greater than last, you get a new full allocation.[0] https://github.com/gcc-mirror/gcc/blob/master/gcc/ada/libgna...
Regarding access values, I listed out some of Ada's various restrictions. Its scope rules prevent referencing objects at deeper levels, objects must be explicitly marked aliased to create an access value to them, and there's far less need for access values (for instance, no pointers are needed to pass parameters by reference). Additionally, Ada offers the ability to dynamically size some objects and reclaim their memory without explicit memory allocation.
After I highlighted these details, ChatGPT admitted it had unfairly evaluated Ada, concluding it's a very safe and robust language, albeit using different techniques than Rust.
I understand the value proposition of Formal Verification with Spark.
But for me the killer features with Ada, thinking specifically of embedded systems is:
- The expressiveness you gain with Ada's Type System
- The Ravenscar profile (very impressive work from a small group of folks in the IRTAW group)
I personally think that AdaCore, and friends, missed an opportunity in the early 2000's to fully embrace open source... they left a big gap which Rust has filled nicely.
I still think Ada is a great programming language. When a question comes up along the lines of: "what's the best programming language nobody's heard of?", or "what's the best programming language that is under used?" Ada is usually my first answer. I think other good answers include F#, <insert LISP flavor>, Odin, Prolog, Haxe, and Futhark (if you're into that sort of thing).
And from the vendor point of view releasing a compiler under libre license allows for concurrents to undercut one on R&D leading to the compiler and related tools certification. So from business point of view it just makes no sense. This is very different from contributing to, say, clang, where a cost of maintaining own closed fork outweighs any disadvantages of contributing.
[2] https://www.adacore.com/press/adacore-announces-the-first-qu...