Rust is supported by the [seL4 Microkit](https://docs.sel4.systems/projects/rust/), which is the core framework enabling LionsOS. LionsOS can currently run components written in Rust, and there are some WIP drivers written in Rust in the seL4 Device Development framework (judging from pull requests).
I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having much success.
It's funny how people always allude to fanatical Rust developers in the most tangential threads, but they never actually turn up and demand we rewrite the entire Kernel in Rust or whatever terrible takes they're alleged to have.
At least someone hasn't complained about it being 'unix like', always without defining what the non-unix-like OS they want would look like, or where the software to run on it would come from.
First, we could start by what UNIX authors did after they considered UNIX done, looking at Plan 9 and Inferno.
Then there are the OSes already done during the 1960 and 1970 outside Bell Labs, as possible ideas.
As from where the software would come from, if we keep recicling UNIX, we will keep getting UNIX regardless of whatever cool features the OS might offer, as most developers are lazy.
Hence why it is great that while Apple and Google OSes have some UNIX there, bare bones POSIX apps will hardly make it into the store.
… except that Rust’s compiler has been qualified for several safety critical standards, with more to come, and has several formal verification tools as well. Amazon even has placed bounties (and paid some) for proving things about the standard library.
Rust is not as immature or evolving in the ways you imply.
Rust is supported by the [seL4 Microkit](https://docs.sel4.systems/projects/rust/), which is the core framework enabling LionsOS. LionsOS can currently run components written in Rust, and there are some WIP drivers written in Rust in the seL4 Device Development framework (judging from pull requests).
I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having much success.
I see you have not met a lot of Rust activists.
Certainly I don't seem to run into as many of them as I'm led to believe exists.
It's funny how people always allude to fanatical Rust developers in the most tangential threads, but they never actually turn up and demand we rewrite the entire Kernel in Rust or whatever terrible takes they're alleged to have.
1 reply →
At least someone hasn't complained about it being 'unix like', always without defining what the non-unix-like OS they want would look like, or where the software to run on it would come from.
First, we could start by what UNIX authors did after they considered UNIX done, looking at Plan 9 and Inferno.
Then there are the OSes already done during the 1960 and 1970 outside Bell Labs, as possible ideas.
As from where the software would come from, if we keep recicling UNIX, we will keep getting UNIX regardless of whatever cool features the OS might offer, as most developers are lazy.
Hence why it is great that while Apple and Google OSes have some UNIX there, bare bones POSIX apps will hardly make it into the store.
Because it is not UNIX like.
It does provide some degree of POSIX compatibility, but it does not dictate architecture.
Rust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
… except that Rust’s compiler has been qualified for several safety critical standards, with more to come, and has several formal verification tools as well. Amazon even has placed bounties (and paid some) for proving things about the standard library.
Rust is not as immature or evolving in the ways you imply.
> Amazon even has placed bounties (and paid some) for proving things about the standard library.
Can you provide some links? Thanks.
1 reply →