7 ms·

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 defin

by init1 1y ago

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 1y ago
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 1y ago
  ... 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.
  - afdbcreid 1y ago
    There is more than one formal verification library for Rust, although none is as integrated as SPARK I believe.
    - johnisgood 1y ago
      How does that work? Why can't other languages have a "formal verification library"?
      - afdbcreid 1y ago
        > 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 1y ago
        Wouldn't C have such a library already if it really was "possible"? You can turn off strict aliasing.
        afdbcreid 1y ago
        Well, I'm not an expert in formal verifications, but there are such libraries, I listed few of them above, you can go and check them. So it is possible. C doesn't have the shared xor mutable rule - with strict aliasing or without.
        johnisgood 1y ago
        I checked them, but I am not convinced and I am not sure why it was brought into this thread. SPARK has industrial-strength, integrated verification proven in avionics (DO-178C), rail (EN 50128), and automotive (ISO 26262) contexts. Rust's tools are experimental research projects with limited adoption, and they're bolted-on and fundamentally different from SPARK. SPARK is a designed-for-verification language subset. Ada code is written in SPARK's restricted subset with contracts (Pre, Post, Contract_Cases, loop invariants) as first-class language features. The GNAT compiler understands these natively, and GNATprove performs verification as part of the build process. It's integrated at the language specification level. Rust's tools retrofit verification onto a language designed for different goals (zero-cost abstractions, memory safety via ownership). They translate existing Rust semantics into verification languages after the fact - architecturally similar to C's Frama-C or VCC (!). The key difference from C is that Rust's type system already guarantees memory safety in safe code, so these tools can focus on functional correctness rather than proving absence of undefined behavior. Bottom line is that these tools cannot achieve SPARK-level verification for fundamental reasons: `unsafe` blocks create unverifiable boundaries, the trait system and lifetime inference are too complex to model completely, procedural macros generate code that can't be statically verified, interior mutability (`Cell`, `RefCell`) bypasses type system guarantees, and Rust can panic in safe code. Most critically, Rust lacks a formal language specification with mathematical semantics. SPARK has no escape hatches, so if it compiles in SPARK, the mathematical guarantees hold for the entire program. SPARK's formal semantics map directly to verification conditions. Rust's semantics are informally specified and constantly evolving (async, const generics, GATs). This isn't tooling immaturity though, it's a consequence of language design.
  - debugnik 1y ago
    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 1y ago
      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 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
- johnisgood 1y ago
  > 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 https://learn.adacore.com as well. [1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#levels-of-software-assurance https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...
afdbcreid 1y ago
(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.

by init1 1y ago

debugnik 1y ago

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 1y ago
... 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.
- afdbcreid 1y ago
  There is more than one formal verification library for Rust, although none is as integrated as SPARK I believe.
  - johnisgood 1y ago
    How does that work? Why can't other languages have a "formal verification library"?
    - afdbcreid 1y ago
      > 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 1y ago
        Wouldn't C have such a library already if it really was "possible"? You can turn off strict aliasing.
        afdbcreid 1y ago
        Well, I'm not an expert in formal verifications, but there are such libraries, I listed few of them above, you can go and check them. So it is possible. C doesn't have the shared xor mutable rule - with strict aliasing or without.
        johnisgood 1y ago
        I checked them, but I am not convinced and I am not sure why it was brought into this thread. SPARK has industrial-strength, integrated verification proven in avionics (DO-178C), rail (EN 50128), and automotive (ISO 26262) contexts. Rust's tools are experimental research projects with limited adoption, and they're bolted-on and fundamentally different from SPARK. SPARK is a designed-for-verification language subset. Ada code is written in SPARK's restricted subset with contracts (Pre, Post, Contract_Cases, loop invariants) as first-class language features. The GNAT compiler understands these natively, and GNATprove performs verification as part of the build process. It's integrated at the language specification level. Rust's tools retrofit verification onto a language designed for different goals (zero-cost abstractions, memory safety via ownership). They translate existing Rust semantics into verification languages after the fact - architecturally similar to C's Frama-C or VCC (!). The key difference from C is that Rust's type system already guarantees memory safety in safe code, so these tools can focus on functional correctness rather than proving absence of undefined behavior. Bottom line is that these tools cannot achieve SPARK-level verification for fundamental reasons: `unsafe` blocks create unverifiable boundaries, the trait system and lifetime inference are too complex to model completely, procedural macros generate code that can't be statically verified, interior mutability (`Cell`, `RefCell`) bypasses type system guarantees, and Rust can panic in safe code. Most critically, Rust lacks a formal language specification with mathematical semantics. SPARK has no escape hatches, so if it compiles in SPARK, the mathematical guarantees hold for the entire program. SPARK's formal semantics map directly to verification conditions. Rust's semantics are informally specified and constantly evolving (async, const generics, GATs). This isn't tooling immaturity though, it's a consequence of language design.
- debugnik 1y ago
  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 1y ago
    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 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
johnisgood 1y ago
> 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 https://learn.adacore.com as well. [1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#levels-of-software-assurance https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...

afdbcreid 1y ago

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