Yeah I was sad about Singularity too. As for C++, yes it doesn't being an absolute guarantee of memory safety, but C is so error prone that it's ridiculous to suggest anything below an absolute 100% guarantee wouldn't be a compelling improvement. C++ was a gigantic improvement in the safety of C (i.e. such that following good coding practices actually gives you legitimate confidence your code is memory-safe) while still having all of its flexibilities, and yet it still got shunned, so I'm unconvinced that a nitpicky language like Rust makes all the difference just because of its formal verification. If kernel folks wanted compiler help with memory safety they could've embraced C++ and gotten most of the way there.