I don't have any particular feelings about Rust, but proponents of Rust contend it is good for systems work, and that its memory safety checks eliminate memory safety issues arrising from safe code and that limiting code that doesn't pass those safety checks to marked areas makes it easier to audit and reason about memory safety leading to fewer memory safety issues in the final product.

An operating system is the essential piece of systems work, so a Rust OS should serve as a demonstration of the efficacy of Rust in systems work. Is the performance on par with contemporary operating systems? Is the code about as easy to understand as contemporaries? Is there a reduction in memory safety issues vs contemporaries?

Positive results from such a project could inspire others to use Rust for more systems work and perhaps integration into other OS kernels and/or key userspace libraries.

Plus, writing an OS is kind of fun.

I am not arguing with your original point about the language. But Singularity is as closed code as it can get and has a bunch of crazy assumptions associated to it (must have .NET installed which rules out most architectures) Can you explain what you like about it? Compared to C, Rust avoids a whole category of memory related bugs

Redox OS is "*NIX written in Rust." Singularity was a complete reimagining of OS architecture from the ground up. It isn't simply "the same ideas but now in Sing#/CLR!" it was an answer to "what if we designed a clean-sheet OS today?" There's a long paper on it here[0].

But keep in mind Singularity is still a toy OS. It has no use-case, and doesn't aim for real-world goals that would make it commercially successful. I just think that even as toy OS's go, it was one of the more interesting ones of recent times.

[0] https://www.microsoft.com/en-us/research/wp-content/uploads/...

> I like Rust, but I don't understand why "OS written in [language]" is a compelling goal within itself.

There's a few good reasons in my mind:

* proof of concept - if a language claims to be a systems language, being able to point to an OS in it is pretty good proof that it's true.

* dogfooding - if there are problems with how the language works for the OS case, they can be highlighted by the OS. (this is similar to self hosting a compiler)

* community building - some folks want to work on a new OS, and doing it in a specific language helps grow both groups and at least introduces them to each other.

Maybe but this is at the cost of worst design..

For me the 'logical' thing to do to build a 'safety first' OS in the 21st century would be: use the seL4 microkernel and then Rust to build the full OS kernel.

Though I don't know if Spectre changed this.

I'm no expert in this domain but it seems to me that RedLeaf (implemented in Rust and formally verified) is vastly superior to seL4. AFAIU RedLeaf is orders of magnitude cheaper to formally verify to a much higher standard[1] while also being significantly more performant[2] and that Rust's properties are key to both of those advantages[1,2]. (Note: I only skimmed [2].)

Edit: It seems RedLeaf is immune to meltdown due to its design while seL4 has meltdown mitigations[2]. I would assume the same goes for spectre, but that would be an assumption on my part. (Note again, I've only skimmed [2] so I can easily be wrong here.)

[1]: https://www.ics.uci.edu/~aburtsev/doc/redleaf-hotos19.pdf

[2]: https://www.usenix.org/system/files/osdi20-narayanan_vikram....

While I don't know anything specific about RedLeaf, I highly doubt that it is completely immune to Spectre. Spectre fundamentally stems from how modern CPUs are designed and the current understanding is that there is no way to fix Spectre. If you're curious, see the paper "Spectre is here to stay: An analysis of side-channels and speculative execution" [0]. Even on fully up to date OSs with the latest version of Chrome, Spectre is still exploitable (see [1]).

[0]: https://arxiv.org/abs/1902.05178 [1]: https://security.googleblog.com/2021/03/a-spectre-proof-of-c...

I must admit that I don't really understand the RedLeaf design if it doesn't use hardware protections you cannot run C or use unsafe Rust "safely"?? Everything in 100% safe Rust isn't going to happen ever so it isn't really a seL4 competitor more a research prototype.

That said I can imagine a two layer system: if you use 100% safe Rust you have a 'fast path' direct access, otherwise you fallback to slower hardware protection.

I'll have a look thanks but note that seL4 is implemented in C because C has a formally verified compiler CompCert which Rust doesn't have..

... not to mention that seL4 was started in 2006, a full four years before Rust was even conceived of. The proof was finished a year before.

The goal is to make a secure operating system that takes lessons from Linux and improves the architecture.