@brendan0x5 So, my guess is: Maybe, but it isn't an obvious win.

Here's why:

Part of the work to prove #seL4 has been to generate a representation (in part, of the portions of the C language that are being used) in another langauge used by the formal prover (Isabelle)[https://cdn.hackaday.io/files/1713937332878112/seL4-whitepaper.pdf].

In order to switch to Rust (or whatever flavor of memory safety you like best), you'd need to re-do that work for your language of choice, including being able to prove that the binaries produced by your compiler accurately represent the source code put into the compiler.

Obviously not impossible, but a boatload of work, and if you've already proven correctness, what win are you looking for in making such a change?

Keep in mind that while there are ~10k lines of code (see above whitepaper) and that sounds like a lot, the kernel doesn't do memory management (for that matter, it doesn't do very much at all, thus "micro"), and 10k lines isn't really that much, programming-wise.

All the kernel is in charge of is "minimal mechanisms for controlling access to physical address space, interrupts, and processor time." [https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html], and in particular "All dynamic allocation in the kernel handled via capability system. No dynamic memory allocation in the kernel!" [https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/workshops/pdfs/20160423-sel4-capabilities.pdf]

I'll admit that I don't know much about memory safe languages, but if there isn't dynamic memory allocation, and if the kernel doesn't do much anyway (everything else is pushed out to unprivileged isolated user-space), I'm curious what you think they could bring to the table.

For clarity, I'm not being sarcastic; I'm still learning about seL4 and am open to learning about new programming languages.

In particular, I think that a programming language designed around a capability system would be a huge win. Keep in mind that the current default is that every programmer acts as though they have a god given right to every resource the system can offer, as they have learned from history and having admin access to every machine they have ever touched.

Or possibly (the ones that have been converted or that have been exposed to systems where they aren't admins and that don't assume that is a personal affront) that access control based security is the pinacle of security / correctness.

For clarity, I've been both of these people, and they are both adorable positions to be wrong from.