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.
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).
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.
Yes, I think most of us are clear that seL4 isn't Unix. But people continue to complain that anything with a Posix layer is Unix-like, and therefore somehow 'bad'. My point was that virtually everyone who complains about this never, ever explains what would have been better to implement, just that it should have been different.
… 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.
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.
I am a “Rust activist” any day of the week. seL4 is awesome and amazing.
11 replies →
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.
3 replies →
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).
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.
Yeah, once again you (you, pjmlp specifically) have missed the point. But thanks for explaining the obvious (once again).
Because it is not UNIX like.
It does provide some degree of POSIX compatibility, but it does not dictate architecture.
Yes, I think most of us are clear that seL4 isn't Unix. But people continue to complain that anything with a Posix layer is Unix-like, and therefore somehow 'bad'. My point was that virtually everyone who complains about this never, ever explains what would have been better to implement, just that it should have been different.
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.
Why would Rust need formal verification tools like https://github.com/rust-lang/miri if the programming language is so safe that it prevents them[1]?!
[1] Undefined Behaviors.
3 replies →
> Amazon even has placed bounties (and paid some) for proving things about the standard library.
Can you provide some links? Thanks.
3 replies →