[LiamPowell]

I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does.

There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers:

1. Having the option to use SPARK for fully verified code provides a superset of the correctness guarantees provided by Rust. As mentioned in the parent comment, Rust focuses purely on memory safety whereas SPARK can provide partial or complete verification of functional correctness. Even without writing any contracts, just preventing things like arithmetic overflows is incredibly useful.

2. Representation clauses almost entirely eliminate the need for the error-prone manual (de-)serialisation that's littered all over Linux driver code: https://www.adaic.org/resources/add_content/standards/22rm/h...

[kevlar700]

Agreed. It would also alleviate the maintenance issue as Ada was designed to reduce software costs. Realistically the obly way this will have any chance is if a few developers were funded full time to work on it. There seemed to be a few full time devs pushing Rust support and some drivers before it was taken seriously. Honestly Ada is the best language that I have seen for drivers and for network stacks or for registers received as bytes. Linux is missing out.

[quietbritishjim]

> 2. Representation clauses almost entirely eliminate the need for the error-prone manual (de-)serialisation that's littered all over Linux driver code:

Do representation clauses let you specify endianess? From a quick glance at that link it didn't appear so. I would imagine that invalidates most use cases for them.

[LiamPowell]

You can specify endianness, but only over the entire record, not an individual field. The way it works is a little complicated: https://www.adacore.com/gems/gem-140-bridging-the-endianness...

[quietbritishjim]

Interesting, thank you. I think per-record is probably good enough for most applications, and less verbose than per-member. But it's not part of the language (that page calls it "implementation specific") and quite recent (that page is undated but references Ada 2012 so must be since then). It wouldn't have helped the Ada project I'm working on, which had an endianess crisis with serialisation a few decades ago.

[Jtsummers]

Ada 95 added bit ordering.

https://www.adaic.org/resources/add_content/standards/95rat/...

https://www.adaic.org/resources/add_content/standards/95lrm/...

[LtWorf]

rust is in the kernel to attract the young developers, which ada does not.

[Lucretia9]

GetIntoGamedev is not old, he's in his 20's. The issue is, is that people are not prepared to trying something if it doesn't look like C or C++.

[LtWorf]

But he's one. See how many people are jumping on the rust bandwagon…

[ksec]

>ended up with Rust in the kernel but not Ada

Linus hated Ada. I suspect he doesn't exactly like Rust either but the Tribe is just too strong within Linux.

[Jtsummers]

Do you have a source for that? I've found his remarks on Pascal and C++ but not Ada.

[ksec]

Linus' opinion on Ada (vs Rust):

> We've had the system people who used Modula-2 or Ada, and I have to say Rust looks a lot better than either of those two disasters.

https://www.infoworld.com/article/2247741/linux-at-25-linus-...

[Ygg2]

> I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada.

Why? Do you program in Ada or Coq?

People can't be bothered to track lifetimes, what makes you think they are ready to track pre/post-conditions, invariants and do it efficiently and thoroughly.

[LiamPowell]

Having the option there is good, even if not everyone uses it. The same thing applies to Rust.

[Ygg2]

For Rust and Ada in the Kernel they need to be accepted by kernel maintainers.

And seeing they can't stand Rust, when its constraints are much weaker than Ada.Spark what chances does it have?

To paraphrase some computer science guru: The cyclical nature of programming languages is all to blame on the collective programmers. Rather than being guided by mathematic rigor, they are guided by a fashion sense.