>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?