[init1]

What exactly is a "type-related disadvantage"?

As far as I'm aware, Ada has a much more expressive type system and not by a hair. By miles. Being able to define custom bounds checked ordinals, being able to index arrays with any enumerable type. Defining custom arithmatic operators for types. adding compile and runtime typechecks to types with pre/post conditions, iteration variants, predicates, etc... Discriminant records. Record representation clauses.

I'm not sure what disadvantages exist.

[debugnik]

References and lifetimes are where Rust wins over Ada, although I agree that Ada has many other great type features.

Access types are unable to express ownership transfer without SPARK (and a sufficiently recent release of gnatprove), and without it the rules for accessibility checks are so complex they're being revamped entirely. And access types can only express lifetimes through lexical scope, which combined with the lack of first-class packages (a la OCaml) means library code just can't define access types with reasonable lifetimes.

Also, I appreciate that Rust is memory safe by default and without toying with a dozen pragmas. Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.

[johnisgood]

... and formal verification is where Ada / SPARK wins over Rust.

I mean, we can go on but I think it quite ends there, as far as safety goes. :D

There is a reason for why Ada is used in industries that are mission-critical.

> Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.

Not really, you can just use Ada / SPARK and it is all checked at compile-time. Look for my comments where I mention Ada.

[johnisgood]

> Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.

I forgot to add a couple of things in my other comment.

You're conflating a few distinct concepts here.

Ada already provides memory safety by default: bounds checks, range checks, and null checks are all on unless explicitly suppressed. Dereferencing a null access value or indexing out of range raises `Constraint_Error`; it never leads to undefined behavior. So Ada does not need a special profile for that kind of safety.

What you seem to be describing - "a profile that guarantees that code can't be the source of erroneous execution" - is closer to what the SPARK subset provides. SPARK can prove the absence of run-time errors (AoRTE) statically using GNATprove, including ownership and lifetime correctness for access types. That is a verification discipline, not a tasking profile.

Ravenscar, on the other hand, is a concurrency profile. It constrains tasking and protected object behavior to make real-time scheduling analyzable and deterministic; it has nothing to do with preventing run-time errors or erroneous execution. It just limits what forms of tasking you can use.

So: Ada itself is already memory-safe by construction, Ravenscar ensures analyzable concurrency, and SPARK provides formal proofs of safety properties. Those are three orthogonal mechanisms, and it sounds like you're blending them together in your comment. Ada performs its safety checks at run-time by default, whereas SPARK allows proving them at compile-time[1].

I encourage you to read the website for which the link can be found below. If you are serious, then you could go through https://learn.adacore.com as well.

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...

[afdbcreid]

(Disclaimer: I know next to nothing about Ada).

> Being able to define custom bounds checked ordinals

That Rust doesn't have (builtin, at least).

> being able to index arrays with any enumerable type

In Rust you can impl `std::ops::Index` and index types, including arrays, with whatever you want.

> Defining custom arithmatic operators for types

Again, definitely possible by implementing traits from `std::ops`.

> adding compile and runtime typechecks to types with pre/post conditions, iteration variants

If you refer to the default runtime verification, that's just a syntax sugar for assertions (doable in Rust via a macro). If you refer to compile-time verification via SPARK, Rust's formal verification libraries usually offer this tool as well.

> predicates

Doable via newtypes.

> Discriminant records

That's just generic ADTs if I understand correctly?

> Record representation clauses

Bitfields aren't available but you can create them yourself (and there are ecosystem crates that do), other than that you can perfectly control the layout of a type.