Ada doesn't do safe dynamic memory deallocation, right? You'd need Ada.Unchecked_Deallocation.
That's fine in cases where you can statically define everything up front (which you can for many of the use cases that people use Ada for), but for a general-purpose OS kernel, it seems like you wouldn't get the level of safety or correctness from Ada that you would from either Rust or C++.
(Disclosure - I'm one of the authors of the prototype mentioned in the thread. I'd happily use Ada or Frama-C if I thought it would solve the problems needed for getting safe code into the Linux kernel, but it doesn't seem like they actually do.)
I think this thread is too narrow on correctness. Plenty of memory issues in C/C++ can be solved by library code i.e. not char buf[...] but std::string. Not raw pointers but RC-pointers. The idea that language strictures alone solve a substantial part of code correctness I think is something that people with more experience in particularly CSP computing ala TLA/SPIN would seriously doubt. And even on the nit pickier things ... RUST is gonna help me write lock-free code with CAS, memory fences? Really?
That's fine in cases where you can statically define everything up front (which you can for many of the use cases that people use Ada for), but for a general-purpose OS kernel, it seems like you wouldn't get the level of safety or correctness from Ada that you would from either Rust or C++.
(Disclosure - I'm one of the authors of the prototype mentioned in the thread. I'd happily use Ada or Frama-C if I thought it would solve the problems needed for getting safe code into the Linux kernel, but it doesn't seem like they actually do.)