While folks keep discussing C vs Rust, what got my attention was MicroPython and Pancake (<a href="https://trustworthy.systems/projects/pancake" rel="nofollow">https://trustworthy.systems/projects/pancake</a>).
Presumably named after Associate Professor John Lions[0], of <i>A Commentary on the UNIX Operating System</i>[1] fame.<p>[0] <a href="https://en.wikipedia.org/wiki/John_Lions" rel="nofollow">https://en.wikipedia.org/wiki/John_Lions</a><p>[1] <a href="https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Operating_System" rel="nofollow">https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...</a>
The mascot it super cute lion too. How can a project do everything so right? I was browsing some popular python libraries and they just slapped on the first image they got out of ChatGPT. It's nice to see care in the craft.
It is <a href="https://www.youtube.com/watch?v=W8Ka_8kHTj4&t=903s" rel="nofollow">https://www.youtube.com/watch?v=W8Ka_8kHTj4&t=903s</a>
It's developed by UNSW Sydney, whose mascot is a Lion. (Specifically, "Clancy the Lion"), so I am guessing it's probably that.
Not presumably, but explicitly. Both in documentation and presentations by seL4 they consistently make a point to mention so.
aka the Lions book
Aussies were supposed to progress with Darbat.<p>It never happened.
if you rearrange the letters, you get the Linos OS.
Very cool! I’m a huge fan of Genode, another OS that runs on SeL4. Does anyone here know how they compare?
On recent news, LionsOS, as of about a week ago (I got notified via their announcement maillist), includes a router/firewall scenario[0].<p>Do not miss Gernot Heiser's recent talk[1] at the seL4 Summit, where among other things he shows seL4 massively outperforming Linux in a web server scenario.<p>0. <a href="https://lionsos.org/docs/examples/firewall/" rel="nofollow">https://lionsos.org/docs/examples/firewall/</a><p>1. <a href="https://youtu.be/wP48V34lDhk" rel="nofollow">https://youtu.be/wP48V34lDhk</a>
> To be successful, many more components are needed.<p>What is the purpose of this OS ? Can it mint Bitcoin ? Can it do fluid dynamics simulation ? Can it act as an interface to a database ? Can it host a database ? Is it interactive ? What kind of interface it presents to the user ?
One application would be safety and security critical real-time systems that also need significant amount of processing power
That’s a rather luridly practical view that’s entirely out of sync with academia and basic research that provides tangible benefits much further down the line.
Those are applications, not operating systems. With occasional exceptions, you can run any application on any operating system.
There is an example of interface in the docs: <a href="https://lionsos.org/docs/examples/kitty/" rel="nofollow">https://lionsos.org/docs/examples/kitty/</a>
Could have been done for fun. You wouldn't understand.
no operating system does. That's application software you're thinking of. So no, it can't. But neither can windows, linux, macos, solaris, templeOS or any others
Yeah, Linus, what's the point?
Mountain Lion is calling and wants its name back.
Oh no, it's written in C and not Rust. The blasphemy!
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.
Rust is supported by the [seL4 Microkit](<a href="https://docs.sel4.systems/projects/rust/" rel="nofollow">https://docs.sel4.systems/projects/rust/</a>), 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.<p>Then there are the OSes already done during the 1960 and 1970 outside Bell Labs, as possible ideas.<p>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.<p>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.
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.<p>Rust is not as immature or evolving in the ways you imply.