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