[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.

[debugnik]

Only if SPARK is powerful enough to verify the code you need to write in the first place, which from my experience with SPARK is not a given as soon as access types are involved. Also Rust doesn't need to exclude high level language features just to prove memory safety, whereas SPARK can't even verify any use of controlled types.

If SPARK really were enough, I'd just write all Ada in SPARK of course.

[johnisgood]

You're partly right that SPARK is conservative, but the claim that it "can't handle access or controlled types" is misleading.

SPARK does support Ada access types (pointers) under a formal permission/ownership model added to GNATprove in recent years. This system - drawn from Rust's borrow-checker ideas - enforces a Concurrent Read, Exclusive Write (CREW) discipline. It enables verification of typical pointer-based structures (singly-linked lists, trees, other acyclic data) via ownership transfers and borrows that the prover can reason about automatically[1]. So long as you follow the ownership rules (no uncontrolled aliasing, no cycles), GNATprove can verify pointer-based code, ensuring the absence of memory leaks and dangling references.

As for controlled types, SPARK excludes them in the verifiable subset because `Initialize`, `Adjust`, and `Finalize` introduce implicit operations that complicate sound reasoning for the automated prover[2]. However, that doesn’t prevent you from using controlled types - you just need to isolate them. The standard pattern is to define them in a `private` part under `pragma SPARK_Mode(Off)` and expose only SPARK-safe wrappers[3]. The controlled operations still run at runtime, but they are hidden from the proof engine. This way, you retain deterministic finalization and prove correctness for the SPARK-visible interface.

In short: SPARK doesn't "exclude high-level features just to prove memory safety" - it modularizes them. It restricts what the prover sees so proofs remain sound and automatic, but you can still use these features through encapsulation. Rust enforces memory safety through its type system at compile time; SPARK aims to prove memory safety plus richer functional properties (absence of runtime errors, contractual correctness) via formal verification. Their goals differ, and SPARK's restrictions are a deliberate trade-off that enable stronger, machine-checked guarantees for high-assurance software.

If you want me to elaborate on the specifics, let me know. Additionally, see https://news.ycombinator.com/item?id=45494263.

Additionally, I am willing to provide more information about what SPARK typically can prove automatically and why some gaps exist.

[1] Jaloyan, Moy, Paskevich - Borrowing Safe Pointers from Rust in SPARK (permission-based alias analysis)

[2] SPARK 2014 User’s Guide, Language Restrictions (implicit operations, excluded features)

[3] AdaCore SPARK tutorials/blogs - exposing controlled types behind SPARK-safe interfaces

[debugnik]

> permission/ownership model added to GNATprove in recent years.

So recently that last time I tried Alire failed to install me a version of gnatprove that supported it. I hope next time I try it actually works though, because I do like the semantics they came up with from the examples I'd seen.

> that doesn’t prevent you from using controlled types - you just need to isolate them. [...] `pragma SPARK_Mode(Off)`

No need to elaborate, I know that SPARK_Mode => Off is the SPARK equivalent of unsafe in Rust; that is, regular Ada. So yes, it does exclude controlled types, and trying to twist SPARK's lack of semantics for them into a pro is not a good argument IMO.

[johnisgood]

> SPARK_Mode => Off is the SPARK equivalent of unsafe in Rust

As I said before: structurally, yes - both mark an implementation as opaque to the verifier/compiler. Semantically, though, SPARK is proof-driven: the verified interface still generates obligations for all callers, and the off-proof body is modularized. Rust's `unsafe` lifts restrictions, but does not automatically enforce correctness across the boundary. That distinction is why SPARK can provide whole-program, machine-checked guarantees while `unsafe` only shifts responsibility to the programmer.

... but I have already said this.

[afdbcreid]

There is more than one formal verification library for Rust, although none is as integrated as SPARK I believe.

[johnisgood]

How does that work?

Why can't other languages have a "formal verification library"?

[afdbcreid]

> How does that work?

Usually taking the IR (MIR) from rustc and translating it to a verifier engine/language, with the help of metadata in the source (attributes) when needed. E.g. Kani, Prusti, Creusot and more.

> Why can't other languages have a "formal verification library"?

I don't think there is a reason that prevents that, and perhaps some have, however it turns out that modelling shared mutability formally is really hard, and therefore the shared xor mutable rule in Rust really helps verification.

[johnisgood]

Wouldn't C have such a library already if it really was "possible"? You can turn off strict aliasing.

[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.