If Ada is already *very* safe, why Rust?

#42

This is a comparison of Rust to Ada, you’re closing this because of what exactly?

#43

The thread is not closed. Just reminding people to keep it focused on Rust comparisons and not to wander too far into other Ada topics.

5 Likes
#44

Because either Ada’s ecosystem is lacking, or Google search is terrible when it comes to finding Ada libraries, which is equally worse to be honest.

How do I create a tar file in Ada? I looked for “ada create tar file” and “ada tar library” and got nothing on the first page of Google.

Rust strength also comes from the “marketing strategy” of early actors which made Rust well-known in a very short span of time. I knew Rust features and strength even before writing my first line of Rust. Also, it has a very strong emphasis on the open-source community.

On the other hand, Ada… Well, I read a paper about it years ago so I know some things about it, but needless to say that that’s not a language that “sells itself” very well. Lack of advertising leads to misconceptions, and misconceptions lead to not using the language.

#45

Googling is a pain, tbh, try: -disabilities -american -australian -dentist -oh

Yup.

#46

Cool; I’m at somewhat of a disadvantage in that case though: I haven’t ever used Rust. Though this particular topic interests me for several reasons: (1) Ada is my main programming language, (2) I am interested in language-design, and (3) I’m on the ARG.

This is one issue that I have with AdaCore — they market Ada in such a way that it seems like they’re saying Ada is only applicable to the high-integrity/-safety world, almost excluding the general programming world — but, if I’m being honest, I really don’t know how/if I could do better with marketing

1 Like
#47

In my last job there was a colleague who was involved in a lot of Ada projects. I have never used Ada so I just have to trust him:

He told me once that Ada is a very nice general purpose language but he wouldn’t write an office suite or a web browser in Ada. It’s not the main focus of Ada.

Rust on the other hand has the focus to be a general purpose programming language.

He also told me that Ada compilers aren’t allowed to do certain kinds of optimizations that for example c, c++ (and Rust and other PL via LLVM) are doing.

Thus in theory you cloud write a 3D-game engine with Ada. But it would never be as efficient / fast as one written in c / c++ / Rust.

I really don’t know how/if I could do better with marketing

Well you (or s.o. else) could write a web browser, an office suite or a 3D-game engine in Ada and show everyone that it is possible :wink:

#48

I’ve just had this confirmed on the cla list:

In Ada, the principle is that the compiler has an obligation of result,
i.e. that the “external effect” (see 1.1.3(9)) of the compiled program
must be the same as the effect defined by the canonical execution.

Basically, this means that the compiler can do any optimization provided
the result is correct. Going farther than that would mean allowing the
compiler to generate incorrect programs…

#49

@Lucretia that dos not confirm that “Ada compilers aren’t allowed to do certain kinds of optimizations that for example c, c++ (and Rust and other PL via LLVM) are doing”. Quite the opposite. Rust, C and C++ compilers are bound by the same contract:

the “external effect” of the compiled program must be the same as the effect defined by the canonical execution [of the source program].

2 Likes
#50

Well, the specs are freely available for anyone to look at and you can find what you can and cannot do in there. I’ve never seen anything that says you can’t do optimisations in those docs.

#51

Are you talking about Rust or Ada specs/docs? A Rust spec is still very early work-in-progress.

I didn’t say you cannot do optimizations, I just said that the rules for optimizations are the same in Rust and Ada (and any other programming language out there, really): you may only optimize if that does not change program behavior.

You gave a quote to “confirm” that “Ada compilers aren’t allowed to do certain kinds of optimizations”. But your quote doesn’t confirm that in any way.

#52

Just a side note: C++ has a thing called copy elision that is considered an optimization, but that do change the program behaviour.

Under the following circumstances, the compilers are required to omit the copy and move construction of class objects, even if the copy/move constructor and the destructor have observable side-effects. The objects are constructed directly into the storage where they would otherwise be copied/moved to.

However, it’s more about language model and its semantics, rather than bit fiddling one may find in LLVM optimizations. I believe such things are forbidden in Ada by design, whereas cautious optimizations may be done.

#53

There is not really much difference in performance of C++, Ada, and Rust. You can look at https://benchmarksgame-team.pages.debian.net/benchmarksgame/

The difference may come from use of unsafe code, Ada I believe doesn’t have unsafe code feature.

#54

Examples of common usage of compiler pragmas would be to disable certain features, such as run-time type checking or array subscript boundary checking, or to instruct the compiler to insert object code in lieu of a function call (as C/C++ does with inline functions).

#55

A lot of Ada advocates believe that Ada provides memory safety if you do not use pointers. This has also found its way into many descriptions of Ada.

But it is simply not true. Here is one counter-example that only uses core language features:

I’ve written a fairly literal unsafe Rust translation, too.

5 Likes
#56

The article is interesting, but I am genuinely concerned by the widespread belief: where have you encountered that? That the so aptly named unsafe Rust is able to be unsound is not new :smile: and I expect people to be aware of that :grimacing:

By the way, I have taken the liberty to clean up your example a bit (no need for Uncopyable, and using ptr::read requires to mem::forget elsewhere, which your code did not (so your code actually had another soundness issue)):

/// To show unsoundness we implement type transmutation
unsafe fn magic<'a, A : 'a, B : 'a> (a: &'a A) -> &'a B
{
    enum Magic<'a, A : 'a, B : 'a> {
        A(Option<&'a A>),
        B(Option<&'a B>),
    }

    let mut magic = Magic::B(None);
    let b_ptr = match magic {
        | Magic::B(ref at_b) => at_b as *const Option<&B>,
        | _ => unreachable!(),
    };
    #[allow(unused_assignments)] {
        magic = Magic::A(Some(a));
    }
    (*b_ptr).unwrap() // <- unsafe-ly dereference the invalid b_ptr
}

Now, you say that no dangling pointers are involved, but I think that it depends on the definition of dangling pointer. Sure, the pointee *b_ptr has not been freed, but since it has mutated / changed in shape since the moment the reference/pointer was created that could count as dangling.

But in any case I think we are both saying the same thing: lifetimes are paramount for soundness :slightly_smiling_face:

#57

I am confused as to why this can’t just be done with some pointer casts, like so

unsafe fn magic<A, B>(a: &A) -> &B
{
    &*(a as *const A as *const B)
}

or

unsafe fn magic<A, B>(a: A) -> B
{
    let b = std::ptr::read(&a as *const A as *const B);
    std::mem::forget(a);
    b
}
#58

The idea was to avoid casts / transmutes I think: “enums as safe? unions”

1 Like
#59

Is it not true though, that SPARK doesn’t have this hole?
For instance, since you cannot have functions with side-effects in SPARK, your example would not pass the SPARK validation (examiner).

#60

Since nobody else responded, I might as well.

struct Foo(u32);
...
let foo_box = Box::new(Foo(42u32));

This…

  1. Declares a single-element data structure named Foo (struct Foo) containing a 32-bit unsigned integer which, being the first/only element in a “tuple struct” (no explicit field names), will be given the field name 0. (In Rust, such single-element structs are commonly used to define new types that have the same in-memory representation but will not be treated as equivalent by the compiler and will have their own different set of available methods.)
  2. Creates a heap-allocated (Box::new) instance of it containing the number 42 (42u32 is an integer literal that’s being explicitly declared as a u32 rather than type-inferred.) and stores the owning reference to it in the variable foo_box.
  3. When foo_box goes out of scope, the memory will be freed.
1 Like
#61

Thank you for the explanation.