>Ada maybe isn't very well adapted to kernel code? From what I know of Ada, doesn't it get it's memory safety from either a GC or not freeing memory entirely? That is -- ownership rules are pretty new to Ada/SPARK.

I think GC is optional with Ada, as far as I know the memory safety comes from raising exceptions (or refusing to compile) when it detects memory-unsafe operations (array bounds checking etc).

>C-style syntax and community interest also favor Rust.

That's fair, C-like languages are instantly familiar with software people and rust seems to have a more hip image than old man fuddy-duddy Ada.

>This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance?

I'm not arguing for Ada over Rust (I'm not a software guy) so I don't mean it as a red herring, but wouldn't a suite of static verification tools and a formally verified compiler require a spec to be tested against?

Re: spec, not if the spec is implementation (and project's values) defined. I mean -- the Rust project has a ridiculous # of tests which define language behavior without having an ISO standard. Yes, implementation defined behavior in C is usually a place where C compiler engineers trade safety for speed. Yes, that's usually a bad trade. However, I'd look at this situation re: Rust vs. C in a different way though -- the Rust project's values are why defining a standard is less important.

I think a spec is often a red herring because a bunch of folks living in the slum of C, when asked if they would all like to move into Rust's nice 3 bedroom by the park, instead always seem to ask: Wouldn't it be better to form a committee about building us a cathedral? Ada might be better. Someone should try it, but until then I'll take Rust.

It's always fun to read peoples drive-by opinions about the only decent language IMO. Ada is highly compatible with C code. For dynamic allocations with "ownership" there is the concept of memory pools which CAN use a GC if thats how you choose to implement the pool allocator.

Haha, I'm sorry if it seemed like I ever knew what I was talking about. I thought asking questions would make it clear that I don't.

Remain interested in the potential advantages of Ada compared to Rust for Linux kernel development, if you would care to point me in the right direction.