It takes a while to write a stable OS, because a lot of things that we use in our helpful libs can't be used in Kernel space. I'm thinking of taking some time and trying to help a Rust OS project.
http://src3.org/#RHEL6-2.6.32+220.el6/lib/
or for example Linux Kernel "string.h" (with fun ifdef) http://src3.org/#RHEL6-2.6.32+220.el6/include/linux/string.h
I'm sure reaching Rust 1.0 will speed things up.
Someone posted their Rust kernel https://github.com/lexs/rust-os
It would take a very long time for that to be even possible. The hardest part of writing an OS today is more about the amount of hardware out there to support and getting users. There are a couple of approachs to mitagate this thou.
1) Work well in a niche, this has worked well for L4, QNX, VxWorks etc, but doesn't make the OS very visable to most people.
2) Run on top of an existing virtulisation plaform to minimise the hardware support needed, butby doing that you also reduce the impact of working in a safer language.
I guess you could argue that "better" doesn't have to mean relevent to end users/devs, a bit of an ivory tower approach thou. Otherwise you are looking at several years of work
As it turns out, very few people are interested in having software that works.
(Moreover, rust itself may have bugs, or there could be bugs in unsafe code in the standard library. The amount of trusted infrastructure is much smaller for SEL4, I suppose if you compile it with compcert, I imagine it's quite small)
The worst case latency is also part of the proof for SEL4-- which is a kind of correctness you cannot achieve via rust (even ignoring overhead).
There are many elements of program correctness beyond memory safety. The developers of rust generally eschewed concerns about other kinds of correctness. For example, your integer types may overflow and your algorithms could fail to work as a result. SEL4's proofs show the operation of the software match its specifications completely (given some assumptions), it's really far far beyond the memory safety promises of rust.
For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute.
But you're right that bugs in the compiler could produce safety issues.
Perhaps not, but in a kernel you'd have plenty of your own unsafe code.
SEL4 doesn't.
There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4.
As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.
A Rust based kernel could be a *nix, and do everything from desktops to server. It would be developer friendly in the same way Linux or Windows is. Plus, the baseline safety would be much higher with a Rust based kernel, without having to formally proven everything.
Instead of having all the services required for an operating system in the kernel, the kernel just implements the bare minimum including fast IPC. Things that traditionally are implemented in the kernel (filesystems, device drivers, other modules, etc) are all implemented as services living in userland and are assigned the minimum necessary additional permissions for them to perform their task.
You can build a *nix like system on top of seL4. You can even run Linux itself on top of seL4, with L4 acting as a hypervisor.
An operating system doesn't consist of just the kernel.
No. Most of the huge development was in developing proofs for C. The developers now find that development is easier than just using C directly. The process is to write it in a high level specification language, then when you're done messing around and know you have it how you want it, translate it to C by hand and the proofs will tell you that you did it right (or wrong).
>It doesn't seem to have the feature you expect from kernels these days.
It has exactly the features we expect from kernels these days. The features we do not expect from kernels these days but did expect from them 30 years ago are available in a library where they belong.
>A Rust based kernel could be a *nix
So can any L4. Why would "start from absolutely nothing" be easier than "start from an existing microkernel"?
L4 is fantastic, by the way.
No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide.
>because it would have far fewer segfaults and the like
SEL4 can not segfault, that's the point. It isn't fewer, it is zero.
>but clear I was thinking that we can start with a Rust kernel and build on top of that.
Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.
Presumably you'd want formally verified versions of at least the network device driver... otherwise process isolation might be violated.
The reason very few people care is that "works" is not a binary, but obviously a continium -- and people inherently understand diminishing returns...
Especially when the "works" they care about is getting shit done, by having access to software (including proprietary), drivers, a community, vendors, etc.
The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
That's however orthogonal to what I wrote, I think.
It's not like it has a software ecosystem, community, drivers, etc, to be adopted over any major OSes as something that "all others being equal" is also "formally verified".
And yet your post can be summarized as "I am not aware of the usage of L4 microkernels".
>The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
I'm talking about people in general, prefaring their mainstream OS of choice over some platform based on L4.
Not about L4 users opting for this or that implementation.
The parent talked about people in general not caring for software quality, while those L4 users are highly specialized enteprises and businesses making a choice.
Not necessarily. If there is a formal model of a specification, and a piece of software provably implements that specification, then that is an example of software that works in a very clear, not-a-contiuum sense.
Yes, and we know what the quality there is.
If that's your attitude, you probably don't work in or near the industries that would have the budget or requirements to care about the seL4. I have, and it would be considered, without a doubt.