I use Ada professionally and enjoy how expressive and powerful the language is in cleanly representing modular design and preventing errors. This is especially true with all of the features that came with Ada 2005 and Ada 2012.
I have no doubts about Ada or SPARK. I am questioning what is needed to make a new operating system design viable other than "it's written in Ada". What is needed to make an operating system that can be as good as or better than the POSIX-based operating systems that dominate computing.
I personally think AdaOS is very compelling if you want a unique perspective on memory safety at such a large scale.
It's much more than a "favorite" language and certainly not even in the same realm of application as a language such as C.
Misra C in contrast to Ada, now that's a comparison. Not D, C++, etc.