https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust

Ferrous Systems is apparently a Rust support company based in Germany.
From the linked page:

"Ferrous Systems and AdaCore are announcing today that they’re
joining forces to develop Ferrocene - a safety-qualified Rust
toolchain, which is aimed at supporting the needs of various
regulated markets, such as automotive, avionics, space, and
railway."

No mention about whether there will be any type of FOSS or community
release. No word on whether the compiler and/or toolchain will be based
on the existing stuff, or something new. Wonder how they will
safety-certify anything in Rust when the language itself doesn't even
have a formal spec. But, it is an interesting development.

Is the writing on the wall for Ada?

On 02/02/2022 08:57, Paul Rubin wrote:
> https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust
>
> Ferrous Systems is apparently a Rust support company based in Germany.
> From the linked page:
>
> "Ferrous Systems and AdaCore are announcing today that they’re
> joining forces to develop Ferrocene - a safety-qualified Rust
> toolchain, which is aimed at supporting the needs of various
> regulated markets, such as automotive, avionics, space, and
> railway."
>
> No mention about whether there will be any type of FOSS or community
> release. No word on whether the compiler and/or toolchain will be based
> on the existing stuff, or something new. Wonder how they will
> safety-certify anything in Rust when the language itself doesn't even
> have a formal spec. But, it is an interesting development.
>
> Is the writing on the wall for Ada?

I see this going one way, Ada loses out as the Rust side uses AdaCore to
get what they want.

If possible please tell what Rust has to offer over Ada.
From a quick look at the Rust book it seemed weaker in structured programming, generic programming, type system.
Thanks.

Paul Rubin <no.email@nospam.invalid> writes:

> https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust
>
> Ferrous Systems is apparently a Rust support company based in Germany.
> From the linked page:
>
> "Ferrous Systems and AdaCore are announcing today that they’re
> joining forces to develop Ferrocene - a safety-qualified Rust
> toolchain, which is aimed at supporting the needs of various
> regulated markets, such as automotive, avionics, space, and
> railway."
>
> No mention about whether there will be any type of FOSS or community
> release. No word on whether the compiler and/or toolchain will be based
> on the existing stuff, or something new. Wonder how they will
> safety-certify anything in Rust when the language itself doesn't even
> have a formal spec. But, it is an interesting development.
>
> Is the writing on the wall for Ada?

Yes. And it says:

As long as people care about quality software engineering, they will
use Ada.

:)

--
-- Stephe

On 02/02/2022 15:29, Marius Amado-Alves wrote:
> If possible please tell what Rust has to offer over Ada.
> From a quick look at the Rust book it seemed weaker in structured programming, generic programming, type system.
> Thanks.

Don't know why you're asking me, but to me, not a lot, only the borrow
checker stuff.

> Is the writing on the wall for Ada?

Don't worry too much, people said that already more than 30 years ago...
But perhaps the company will rebrand itself RustCore :-) ?

Gautier write-only address <gautier_niouzes@hotmail.com> writes:
> But perhaps the company will rebrand itself RustCore :-) ?

If the new IDE is called Oxide, watch out ;-).

"Luke A. Guest" <laguest@archeia.com> writes:
> I see this going one way, Ada loses out as the Rust side uses AdaCore
> to get what they want.

I don't think this is two companies merging. It's two companies working
jointly on a particular product. Idk any more than the press release
though.

Regarding Rust vs Ada, I've never heard anything from anyone who is a
real expert at both. Superficially it looks to me like Rust's type
system really is more precise than Ada's in general, although it doesn't
have integer range types. In other stuff like modules, Ada is probably
still ahead.

On 02.02.22 16:29, Marius Amado-Alves wrote:
> If possible please tell what Rust has to offer over Ada.
> From a quick look at the Rust book it seemed weaker in structured programming, generic programming, type system.
> Thanks.

Embedded systems reportedly still mostly use C.
Consequently, C is the thing to which a language's merits must
be compared. If Rust managers manage to persuade C shops
to use Rust, the this is a reasonable attempt at improving C based
program production. If Ada influence the process, then
it has had a purpose. :-)

Perhaps it is easier to add guarantees to Rust programs
than to C programs. Also, C programmers might feel more
at home when using Rust. Java programmers also, even when
it is just curly braces.

On 02/02/2022 20:06, Paul Rubin wrote:
> "Luke A. Guest" <laguest@archeia.com> writes:
>> I see this going one way, Ada loses out as the Rust side uses AdaCore
>> to get what they want.
>
> I don't think this is two companies merging. It's two companies working
> jointly on a particular product. Idk any more than the press release

I know. I never said otherwise. I just said I think that one will use
the other and not in Ada's favour.

> though.
>
> Regarding Rust vs Ada, I've never heard anything from anyone who is a
> real expert at both. Superficially it looks to me like Rust's type

I've heard nothing either, only keep seeing rust people demanding to
know what Ada's good for and how it compares to Rust. Er, try learning
both and you'll see?

> system really is more precise than Ada's in general, although it doesn't

How is it?

> have integer range types. In other stuff like modules, Ada is probably

Apparently, they have ranges as templates, can't see how that compensates.

> still ahead.

Ada's ahead in most things.

"Luke A. Guest" <laguest@archeia.com> writes:
> [Ada vs Rust] Er, try learning both and you'll see?

It's a big effort to become expert at either, let alone both. Basic or
superficial knowledge isn't helpful for such comparisons. I've read
"Ada Distilled" (Ada 95 version) but still have no clue understanding
most of the Ada discussions in this newsgroup, so there is a big gap
between basic and advanced knowledge of Ada.

>> system really is more precise than Ada's in general, although it doesn't
> How is it?

From what I've heard, Rust's type system is similar to Haskell's.
Haskell's type system can verify stuff just by typechecking, that might
be doable in Ada using SPARK and maybe an external proof assistant, but
not with just types. Example: a red-black tree using Haskell GADT's
(Generalized Algebraic Data Types):

https://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

> Ada's ahead in most things.

Idk, I'd like to know more. I've never done anything serious in Ada and
nothing at all in Rust, but C++ seems a lot more fluid than Ada, and
Rust is supposed to compare well with C++. C++ of course is terrible in
terms of reliability but I'm only referring to the effort needed to bang
out a chunk of code.

On 03/02/2022 02:20, Paul Rubin wrote:
> "Luke A. Guest" <laguest@archeia.com> writes:
>> [Ada vs Rust] Er, try learning both and you'll see?
>
> It's a big effort to become expert at either, let alone both. Basic or
> superficial knowledge isn't helpful for such comparisons. I've read

You don't need to learn both languages inside and out. You pick a
project and implement it in both languages, that project has to be
specific to what you are wanting to know about whether it's binding or
tasking or whatever, Ultimately with Ada, you can get by knowing the Ada
subset and the representation clauses and do most of what you need to do
to compare to another language, obviously if you want to compare
tasking, you need to go further.

> "Ada Distilled" (Ada 95 version) but still have no clue understanding
> most of the Ada discussions in this newsgroup, so there is a big gap
> between basic and advanced knowledge of Ada.

Learn the basic part, it's equivalent to Pascal with proper type ranges,
Pascal only has subtypes iirc. That's the main part of the RM, no
annexes, you can do without access and tagged/controlled types to start
with. At uni, we didn't even touch on tagged types, but used controlled
types, it is possible.

>>> system really is more precise than Ada's in general, although it doesn't
>> How is it?
>
> From what I've heard, Rust's type system is similar to Haskell's.
> Haskell's type system can verify stuff just by typechecking, that might

So it's no different than a C++ compiler checking against classes or a
variant of C with strong typing? Still no ranges, subranges, ranges with
holes in, etc. This is where the power is.

> be doable in Ada using SPARK and maybe an external proof assistant, but
> not with just types. Example: a red-black tree using Haskell GADT's
> (Generalized Algebraic Data Types):
>
> https://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

I don't know Haskell. Uni did a shit job at teaching functional, and
logic languages.

>> Ada's ahead in most things.
>
> Idk, I'd like to know more. I've never done anything serious in Ada and
> nothing at all in Rust, but C++ seems a lot more fluid than Ada, and
> Rust is supposed to compare well with C++. C++ of course is terrible in
> terms of reliability but I'm only referring to the effort needed to bang
> out a chunk of code.

1. What do you want to do?
2. Come into #Ada and get help.
3. Rewrite it in Rust.
4. Ada is comparable to C++.
4a. Ada > C++ in many ways.

"Luke A. Guest" <laguest@archeia.com> writes:
> You don't need to learn both languages inside and out. You pick a
> project and implement it in both languages,

Not realistic, as the saying is that it's possible to write Fortran in
any language. What I want to see is proper idiomatic usage of both
languages as experts would write them. Also, it seems to me that one of
Ada's big strengths is its modularity, e.g. the separation of
specification from implementation. And that makes itself felt more with
large programs than small ones. A beginner or tryout project wouldn't
exercise this.

> [Ada] Learn the basic part,

I think I have done that, but there is a heck of a lot more.

> [Haskell] So it's no different than a C++ compiler checking against
> classes or a variant of C with strong typing?

It is very different from either of those.

> Still no ranges, subranges, ranges with holes in, etc. This is where
> the power is.

No not really, especially since Ada doesn't enforce ranges with (static)
type checking, although it is sometimes possible in SPARK. Range types
are a nice Ada feature but only "where the power is" if you haven't used
anything else ;). Anyway, you can implement ranges (with runtime
checks) in C++ or Haskell with a bit of pain.

>> Example: a red-black tree using Haskell GADT's
> I don't know Haskell. Uni did a shit job at teaching functional, and
> logic languages.

Well are you familiar with red-black trees? They are a data structure
similar to B-trees which you may have seen. Basically the trees have
nodes that are coloured either red or black, and there are some rules
such as that internal red nodes can have only black children, and that
enforces some invariants that keep the trees balanced so that lookups
and updates are guaranteed to run fairly fast.

Now these trees have been implemented in many languages, and if you look
at almost any implementation, there is usually a test suite or internal
debugging code to make sure that the invariants are preserved after
doing an update. It is quite easy to make a mistake after all. But the
Haskell code doesn't have those tests. Why not? Because the invariants
are enforced by the datatype! If you make a mistake and mess up an
invariant, your code won't compile! It's the difference between
checking a subscript at runtime, and verifying that it in range with
SPARK. SPARK lets you get rid of the runtime check. Haskell's type
system is able to do similar things.

> 1. What do you want to do?

I have too many obligations and wannado projects to embark on anything
well suited for either Ada or Rust right now, unless someone is paying
me. Also, I see Ada and Rust not really aiming at the same areas. I
think of Ada as being more for control programs (they might compute a
lot, but tend not to make complex use of dynamic memory allocation)
while Rust is the opposite (handling dynamic allocation reliably is a
big part of the design motivation).

> 4. Ada is comparable to C++.
> 4a. Ada > C++ in many ways.

I don't see Ada and C++ as really comparable. Ada > C++ in reliability
for sure, but C++ > Ada in convenience a lot of the time.

Particularly, a lot of effort in Ada programming goes into making
programs never crash. For example, if the program runs out of memory
during operation it might crash, so Ada programs are often written to
never allocate new memory after a startup phase. In C++ or Rust, it's
important not to get wrong answers like 2+2=5, but if your program runs
out of memory and crashes, go get a bigger computer. So idiomatic C++
and Rust programming uses dynamic allocation freely, and that makes some
kinds of programming more convenient, at the expense of tolerating
possible crashes.

Den 2022-02-03 kl. 05:22, skrev Paul Rubin:

> Particularly, a lot of effort in Ada programming goes into making
> programs never crash. For example, if the program runs out of memory
> during operation it might crash, so Ada programs are often written to
> never allocate new memory after a startup phase. In C++ or Rust, it's
> important not to get wrong answers like 2+2=5, but if your program runs
> out of memory and crashes, go get a bigger computer. So idiomatic C++
> and Rust programming uses dynamic allocation freely, and that makes some
> kinds of programming more convenient, at the expense of tolerating
> possible crashes.

That depends on the domain. Perhaps it is true in embedded.
I use Ada for large systems, talking to databases,
and lots of administrative work. On a win/Unix server.
We would not dream of pre-allocate memory at startup.
We allocate and dispose as needed.

--
Björn

"Luke A. Guest" <laguest@archeia.com> writes:

> At uni, we didn't even touch on tagged types, but used controlled
> types

Of course controlled types are implemented as tagged types. ISTR Dmitry
objecting to this, I think he was right (philosophically; I've no idea
about the practicality of alternate approaches).

On 03/02/2022 11:30, Simon Wright wrote:
> "Luke A. Guest" <laguest@archeia.com> writes:
>
>> At uni, we didn't even touch on tagged types, but used controlled
>> types
>
> Of course controlled types are implemented as tagged types. ISTR Dmitry

We had a book with a reading guide. We weren't shown the specs showing
the type of controlled/limited_controlled. So, when you don't have that
information and only know that you can derive from it and then implement
2 or 3 subprograms, you don't need to know about OOP in Ada.

Just like we didn't touch generic packages until much later in the year,
generic subprograms, yeah, because u_d was required early on.

> objecting to this, I think he was right (philosophically; I've no idea
> about the practicality of alternate approaches).

How else would you do controlled types?

On Wednesday, 2 February 2022 at 15:29:13 UTC, amado...@gmail.com wrote:
> If possible please tell what Rust has to offer over Ada.

A very nasty syntax, and there's an annoying thing where it moans about what you've called your project.

TBH that's about as far as I got with Rust; I can't be doing with pedantic restrictions that have no technical benefit (as far as I can see).

"Luke A. Guest" <laguest@archeia.com> wrote in message
news:stgj3j$12g8$1@gioia.aioe.org...
> On 03/02/2022 11:30, Simon Wright wrote:
>> "Luke A. Guest" <laguest@archeia.com> writes:
>>
>>> At uni, we didn't even touch on tagged types, but used controlled
>>> types
>>
>> Of course controlled types are implemented as tagged types. ISTR Dmitry
>
> We had a book with a reading guide. We weren't shown the specs showing the
> type of controlled/limited_controlled. So, when you don't have that
> information and only know that you can derive from it and then implement 2
> or 3 subprograms, you don't need to know about OOP in Ada.
>
> Just like we didn't touch generic packages until much later in the year,
> generic subprograms, yeah, because u_d was required early on.
>
>> objecting to this, I think he was right (philosophically; I've no idea
>> about the practicality of alternate approaches).
>
> How else would you do controlled types?

Ada 9x originally had a bunch of magic attributes (similar to streaming). It
was very complex and got dumped in the dustbin during "scope reduction".
Later on, some of us were bemoaning that a critical feature (finalization)
had gotten lost in Ada 9x, and Tucker came up with the idea to build it on
top of tagged types as a massive simplification (at the loss of a bit of
power). People often complain that Ada finalization is complex, and it is,
except all of the alternatives are a lot more complex. :-)

Randy.

"Paul Rubin" <no.email@nospam.invalid> wrote in message
news:87v8xwy3y7.fsf@nightsong.com...
....
> Well are you familiar with red-black trees? They are a data structure
> similar to B-trees which you may have seen. Basically the trees have
> nodes that are coloured either red or black, and there are some rules
> such as that internal red nodes can have only black children, and that
> enforces some invariants that keep the trees balanced so that lookups
> and updates are guaranteed to run fairly fast.
>
> Now these trees have been implemented in many languages, and if you look
> at almost any implementation, there is usually a test suite or internal
> debugging code to make sure that the invariants are preserved after
> doing an update. It is quite easy to make a mistake after all. But the
> Haskell code doesn't have those tests. Why not? Because the invariants
> are enforced by the datatype! If you make a mistake and mess up an
> invariant, your code won't compile! It's the difference between
> checking a subscript at runtime, and verifying that it in range with
> SPARK. SPARK lets you get rid of the runtime check. Haskell's type
> system is able to do similar things.

Cool, and most likely useless. OOP is like that in many ways, it lets you
make a bunch of static checks, but to get them, you have to contort your
design in awful ways. And then it is hard to extend, as you have a huge
number of routines to override to get anything done.

I'm convinced that the answer (as much as there is an answer -- always
beware of anyone bearing silver bullets ;-) is in the quality of tools (and
language implementations). In any language with dynamic checks, one can
easily reduce the problem of correctness down to simply proving that no
check fails. So the question is how one can accomplish that with the least
complication for the actual programmer.

Janus/Ada has a switch that can give you a warning for any implicit check
that remains in the code after optimization. Combine that with the
warnings-as-errors switch, and no program that could have a (detectable) bug
can compile. Moreover, in Ada at least, one can introduce essentially any
condition that you want to know as some form of assertion.

To take your red-black example. In Ada, I'd model the tree as a single type
with two subtypes, with Red and Black predicates that enforce the
conditions. Then, using the switches mentioned above, you could only compile
the program if the compiler can eliminate the condition checks (it should be
able to, if they are really complete).

The problem with this scheme, of course, is the quality of the
implementation in terms of eliminating unneeded checks. For now, Janus/Ada
can only do this sort of elimination inside of an extended basic block, and
if something prevents a subprogram from being converted to a single extended
basic block, you're likely to get spurious warnings. (And it only implements
advanced elimination on a few kinds of checks, enough to prove the concept
but not enough to be practical.)

The key for a programming language design is to minimize what Ada calls
erroneous execution (undefined behavior), because it is that possibility
which stop proofs in their tracks (or at least should; at least some tools
ignore that possibility and essentially give garbage results as a
consequence). Ada needs work in that area, but most other languages need
more -- Ada at least detects most problems with dynamic checks.

Anyway, that's my 20 cents (inflation, you know). :-)

Randy.

"Randy Brukardt" <randy@rrsoftware.com> writes:
> In any language with dynamic checks, one can easily reduce the problem
> of correctness down to simply proving that no check fails.

Well sure, but I'd take issue with the word "easily" there. The
invariants for the red-black tree are fairly complicated. Enforcing
them could be done with what I think SPARK calls a "ghost function" or
something like that: a piece of code that is not actually executed, but
is used only by the prover. But, what would the proof look like? I
think it would likely involve some manual work with an external proof
assistant like ISABELLE. That takes quite a bit of effort and knowledge
on the programmer's part.

On the other hand, the RB tree type declaration in that Haskell example
is very natural and appealing even in that old implementation, and using
newer GHC features that have appeared since then, it becomes even nicer.

> So the question is how one can accomplish that with the least
> complication for the actual programmer.

Indeed.

On 04/02/2022 03:20, Randy Brukardt wrote:

>> Just like we didn't touch generic packages until much later in the year,
>> generic subprograms, yeah, because u_d was required early on.
>>
>>> objecting to this, I think he was right (philosophically; I've no idea
>>> about the practicality of alternate approaches).
>>
>> How else would you do controlled types?
>
> Ada 9x originally had a bunch of magic attributes (similar to streaming). It

Now I want to know what these magic attributes were! Were they specific
to a version of OO? Or were they to enable finalization?

"Luke A. Guest" <laguest@archeia.com> writes:

> On 02/02/2022 15:29, Marius Amado-Alves wrote:
>> If possible please tell what Rust has to offer over Ada.
>> From a quick look at the Rust book it seemed weaker in structured
>> programming, generic programming, type system.
>> Thanks.
>
> Don't know why you're asking me, but to me, not a lot, only the borrow
> checker stuff.

Which Ada now has in SPARK (or will soon, at least in GNAT).

--
-- Stephe

On Friday, February 4, 2022 at 4:28:26 AM UTC-6, Luke A. Guest wrote:
> On 04/02/2022 03:20, Randy Brukardt wrote:
>
> >> Just like we didn't touch generic packages until much later in the year,
> >> generic subprograms, yeah, because u_d was required early on.
> >>
> >>> objecting to this, I think he was right (philosophically; I've no idea
> >>> about the practicality of alternate approaches).
> >>
> >> How else would you do controlled types?
> >
> > Ada 9x originally had a bunch of magic attributes (similar to streaming). It
> Now I want to know what these magic attributes were! Were they specific
> to a version of OO? Or were they to enable finalization?

Randy, I agree with Luke: were these intermediate design proposals lost entirely or have they (as still extant) have simply not been released publicly? I suspect that at least some of these attributes have nowadays analogues in C++ smart pointer's & Objective-C/Swift's ARC {strong, weak, plain old data not needing finalization, pointed-to-object ownership, presence of finalization subroutine/function/procedure a.k.a. finalizer/destructor, whether this finalizer in a subtype displaces its parent's finalizer versus this finalizer in a subtype chains its finalizer to all of its ancestors' finalizers unwound from most-derived to underived-root, … and so forth}. Or was Tucker's set of magic attributes going an entirely different direction? That intermediate proposal under consideration back in the 1st half of the 1990s might be a quite interesting read (especially by a reader with an interest in envisioning an Ada-esque analogue of Rust's borrow-checker algorithm).

"Luke A. Guest" <laguest@archeia.com> wrote in message
news:stiv47$bvh$1@gioia.aioe.org...
> On 04/02/2022 03:20, Randy Brukardt wrote:
>
>>> Just like we didn't touch generic packages until much later in the year,
>>> generic subprograms, yeah, because u_d was required early on.
>>>
>>>> objecting to this, I think he was right (philosophically; I've no idea
>>>> about the practicality of alternate approaches).
>>>
>>> How else would you do controlled types?
>>
>> Ada 9x originally had a bunch of magic attributes (similar to streaming).
>> It
>
> Now I want to know what these magic attributes were! Were they specific to
> a version of OO? Or were they to enable finalization?

They were specifically for finalization, and got called automatically in
various places.

Re: Andreas. So far as I know, the documents existed only on paper - there
never were any electronically distributed versions outside of the Ada 9x
team (and possibly the printers). I still have a set of them on my
bookshelf -- I look at them periodically to see where current oddities
appeared in the language (and possibly to get some idea why). [But see
below.]

Looking in the RM 3.0 (the final version was 6.0 for reference), it already
had the tagged type version, but they were derived from an implementation
defined type "Finalization_Implementation", and what became Adjust was named
Duplicate.

Looking in ILS 1.2 (a working document full of ideas but not quite a
complete RM, dated Dec 1992), I can't find any sign of finalization. It must
have been gone by then.

I do have a large number of older documents somewhere in storage, but this
isn't worth digging around in there to find out. Most of those were
incomplete design documents.

You might be able to find something about that design in the Ada 9x mail
archive or in the LSNs (Language Study Notes). You can find them on the
AdaIC archives. =Rooting around in there, there are some promising looking
documents in the "history" section of the AdaIC archives. There is a
directory of stuff called "9x-history"; there probably is interesting stuff
there.
http://archive.adaic.com/pol-hist/history/9x-history/
LSNs are found in:
http://archive.adaic.com/standards/95lsn/
The Ada 9x mail archive (These were known as "MRT comments"):
http://archive.adaic.com/standards/95com/mrtcomments/
The comments of interest here are probably in the ZIPed comments rather than
the more recent ones. (These are text files, I think, even though they don't
have a usual extension.)

Randy.

On Wednesday, February 2, 2022 at 4:29:13 PM UTC+1, amado...@gmail.com wrote:
> If possible please tell what Rust has to offer over Ada.

In my minimally informed opinion after going through parts of the official tutorial a couple of times, what Rust has to offer in general:

+ Memory safety (no leaks, double-free, race conditions*) by default.
- Terrible illegible syntax
+ Safer/more expressive/more modern constructs than C
+ Modern tooling shared by all the community

[*] I guess in a protected-object sense, not in a high-level logic sense. But I don't really know.

The thing is that C is so basic and C++ so prone to shooting yourself in the foot, that Rust hits a middle ground that feels like the best thing since sliced bread to C/C++ programmers wishing for something better. Add to that the true novel contribution to a mainstream language that is memory safety (this is really a new way of thinking when you get into Rust), that if you don't know better (e.g., Ada) it really is overwhelmingly compelling. I'm not surprised at the cult-like following (I mean, we feel like that sometimes in the Ada world, right?) In a sense, Rust is the Ada of a younger generation, and without the baggage.

Of course you sometimes have to use "unsafe" programming evading the borrow checker, just like pointers are sometimes a necessity in Ada; and the legibility becomes truly awful IMHO really fast (to me, this is THE Achilles heel nobody seems to care too much about), but as I said, it has a couple of real selling points over the competition. Of course, if legibility is not your concern because you're used to C++ templating nightmares, you don't feel that particular pain. It's always the same story with Ada; most people don't know better to realize what they're missing.

The whole memory safety thing with the borrow checker goes beyond a gimmick, and it has a solid quality which goes beyond "in Ada you don't need pointers most of the time". It's a compile-time check, and it makes evident that runtime checks are a poor substitute. I'm more ashamed now of the whole anonymous pointers and accessibility surprises in Ada. Yes, SPARK added something similar for pointers, but in Rust it is for all variables. The equivalence in Ada would be not being able to use the same variable in two consecutive calls as an in-out parameter. So it's not the same, besides being only in SPARK.

Not having done anything of real import, I'm not sure how inevitable it is to go unsafe in Rust. My guess is that it will be hidden in libraries just like the Ada standard containers contain some scary pointer use (and I mean that I wouldn't like to have to understand what is going there with the tampering checks etc.) At that point, obviously, you've lost the most solid selling point IMHO. Ada is safer not in a single sense, but as a whole design.

All in all, Rust has one big thing that Ada hasn't, which is the borrow checker.

And that is what how I would summarize it: Rust is better in a single narrow sense, but Ada is better as a general language. Which is, not surprisingly, the consequence of the design motivations for each, which were precisely to have a memory-safe language and a high-integrity-oriented language. So the funny thing is that both have succeeded at their objective.

I really miss not having the time to become proficient in Rust at least to be able to properly compare. I think the memory safety is great to have (and if Ada were designed today, I guess it should play the same integral part, if practical), but Rust is demanding on the programmer in a way that C/C++ aren't, and the maintainability seems suspect, so I don't know how far it will carry Rust into the future. I guess it could absorb a big part of both new C and C++ development.

Boy, can I write a lot sometimes...