And yes, for a really critical system I might consider taking something much simpler and potentially slower but formally proven correct, like seL4.
Google is working on Fuchsia as a new phone / chromebook OS, and it's very much focused on bulletproof security.
One of seL4's points is that security can still be fast, no?
From https://docs.sel4.systems/projects/sel4/frequently-asked-que...
>To the best of our knowledge, seL4 is the world’s fastest microkernel on the supported processors, in terms of the usual ping-pong metric: the cost of a cross-address-space message-passing (IPC) operation.
But within the Linux kernel, you might not need that cross-process IPC at all, so if you're into squeezing every last microsecond of latency, you likely want your entire app running as a monolith in kernel mode.
But if you want security more than top speed, seL4 + a few daemons you write for other OS needs must be fine.
> Our kernel, Zircon, [is not in Rust](https://twitter.com/cpuGoogle/status/1397265884251525122). Not yet anyway. But it is in [a nice, lean subset of C++](https://fuchsia.dev/fuchsia-src/development/languages/c-cpp/...) which I consider a vast improvement over C.
https://blog.cr0.org/2021/06/a-few-thoughts-on-fuchsia-secur...
They are now starting to rewrite OS components in Rust, and I wouldn't be surprised if that happens to Zircon as well, it stared as a C anyway, and thus already suffered one rewrite.
A rewrite usually improves a lot of small things that were found in the previous version. It's like a new major version, even if it does not add new major features.
It's an expensive undertaking, though.
False. Which broken telephone did this come from? The Linux kernel has 0% Rust code in it and has no plans to change that.
(And no, "including experimental Rust support" isn't a plan to change that.)
You don't need Rust to compile the kernel. What's changed now is that you could theoretically write a kernel module in Rust. (But you can, e.g., write a kernel module in C++ too, I've done it before.)
As for seL4, doesn’t that just support my point that highly secure software can be written in any language, even C? seL4 is primarily implemented in C. There “executable spec” is written in Haskell, but the actual kernel that people use is written primarily in C and a little Assembly.
Certainly C and C++ have more footguns than many other languages, but highly insecure as well as highly secure software gets written in all languages. I think coming up with better/easier avenues for digital-security-breach related lawsuits and fines is a better idea than banning specific languages.