8 ms·

This write-up shows that while Ada may have some cultural and type-related disadvantages compared to Rust, Ada seems to generally win the readability contest.

• 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.
    • 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.
• tgv 1y ago
  Compiler speed is quite good, but --as OP-- I've only written AoC in Ada. I think Ada's advantage is the separation between package/module specification and body. If you change a body, the compiler only has to process that file. But the rust compiler must check other files as well, since something in the interface might have changed. But that's a guess. Ada is not necessarily complex, but it does require getting used to. It is a very large language, though.
  • afdbcreid 1y ago
    > If you change a body, the compiler only has to process that file. But the rust compiler must check other files as well, since something in the interface might have changed. That's correct in Rust as well (minus some small warts such as if you add an impl inside, which the Rust team wants to deprecate). In fact rust-analyzer relies on that. The compiler will realize that as well via its sophisticated incremental system, but it does take time to evaluate all the queries, even if all are cache hits.