The Lions Operating System
175 points
18 hours ago
| 11 comments
| lionsos.org
| HN
pjmlp
4 hours ago
[-]
While folks keep discussing C vs Rust, what got my attention was MicroPython and Pancake (https://trustworthy.systems/projects/pancake).
reply
mhd
2 hours ago
[-]
When I read about Pancake, for a very short moment I was hoping for some Elan[1] influences…

1: https://os.inf.tu-dresden.de/L4/l3elan.html

reply
pjmlp
1 hour ago
[-]
Cool, thanks for the link.
reply
cjs_ac
18 hours ago
[-]
Presumably named after Associate Professor John Lions[0], of A Commentary on the UNIX Operating System[1] fame.

[0] https://en.wikipedia.org/wiki/John_Lions

[1] https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...

reply
woolion
15 hours ago
[-]
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.
reply
mlinksva
16 hours ago
[-]
reply
santoshalper
17 hours ago
[-]
It's developed by UNSW Sydney, whose mascot is a Lion. (Specifically, "Clancy the Lion"), so I am guessing it's probably that.
reply
kragen
14 hours ago
[-]
That's also where John Lions taught.
reply
skavi
3 hours ago
[-]

    John Lions is not Lions OS
       is not        is not
         Clancy the Lion
reply
imvetri
9 hours ago
[-]
What does mascot mean
reply
saithound
8 hours ago
[-]
A mascot is an animal figure that represents a product or sports team. For example, the penguin named Tux is the mascot of Linux, and the mascot for the Brisbane Broncos rugby team is the horse named Buck the Bronco.

Mascot is, unrelatedly, also a suburb of Sydney.

reply
snvzz
13 hours ago
[-]
Not presumably, but explicitly. Both in documentation and presentations by seL4 they consistently make a point to mention so.
reply
mzs
14 hours ago
[-]
aka the Lions book
reply
dctoedt
19 minutes ago
[-]
My first thought was to wonder whether it was a Linux offshoot.
reply
spencerflem
17 hours ago
[-]
Very cool! I’m a huge fan of Genode, another OS that runs on SeL4. Does anyone here know how they compare?
reply
panick21_
15 hours ago
[-]
Genode is a framework that can run on many places and on higher level has its own abstractions. Lion OS is based on Microkit the framework developed by the seL4 people that will also be verified. So Lion OS/Microkit is basically the outgrowth of the original seL4 research.
reply
Y_Y
15 hours ago
[-]
Unequal
reply
fithisux
3 hours ago
[-]
"but contains composable components for creating custom operating systems that are specific to a particular task"

like reviving OSfree aka 64bit OS/2

reply
Propelloni
3 hours ago
[-]
It's an OS built around a verified and formally proofed L4 kernel, ie. a microkernel like QNX or MACH. The L4 is a venerable design reaching back at least 25 years, if not longer. It has seen commercial and research uses, e.g. the SIMKO3 mobile phones or the Fiasco distribution. The term "task" is specific here. Running Linux as a custom operating system is a task in microkernel lingo.
reply
fithisux
5 hours ago
[-]
Aussies were supposed to progress with Darbat.

It never happened.

reply
snvzz
13 hours ago
[-]
On recent news, LionsOS, as of about a week ago (I got notified via their announcement maillist), includes a router/firewall scenario[0].

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.

0. https://lionsos.org/docs/examples/firewall/

1. https://youtu.be/wP48V34lDhk

reply
hulitu
15 hours ago
[-]
> To be successful, many more components are needed.

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 ?

reply
oytis
5 hours ago
[-]
One application would be safety and security critical real-time systems that also need significant amount of processing power
reply
qubex
15 hours ago
[-]
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.
reply
lukan
1 hour ago
[-]
Yes, but basic reseach in IT is still not random, but usually has a clear goal, or at least some scope. Like indeed, focus on security? Focus on speed? Focus on reliability? Focus on energy efficency (because it is supposed to run on a tiny embedded device for long).

And the gimmick here seems to be in fact, that it is supposed to be flexibel

"is not a conventional operating system, but contains composable components for creating custom operating systems that are specific to a particular task. Components are joined together using the Microkit tool"

reply
kragen
14 hours ago
[-]
Those are applications, not operating systems. With occasional exceptions, you can run any application on any operating system.
reply
mmooss
5 hours ago
[-]
That begs the point: Each application will often run better on some OSes than on others. For example, high traffic websites usually aren't run on Windows 11.
reply
charlycst
15 hours ago
[-]
There is an example of interface in the docs: https://lionsos.org/docs/examples/kitty/
reply
vrighter
5 hours ago
[-]
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
reply
kjs3
11 hours ago
[-]
Could have been done for fun. You wouldn't understand.
reply
fortyseven
14 hours ago
[-]
Yeah, Linus, what's the point?
reply
lmm
5 hours ago
[-]
Hardly a fair comparison. Linus wanted an OS that would run on his own PC and let him do his Unix homework assignments.
reply
fifticon
4 hours ago
[-]
if you rearrange the letters, you get the Linos OS.
reply
amelius
13 hours ago
[-]
Mountain Lion is calling and wants its name back.
reply
CursedSilicon
11 hours ago
[-]
You mean OS X 10.7 Lion?
reply
gethly
13 hours ago
[-]
Oh no, it's written in C and not Rust. The blasphemy!
reply
aloha2436
13 hours ago
[-]
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.
reply
fooker
11 hours ago
[-]
I see you have not met a lot of Rust activists.
reply
aloha2436
11 hours ago
[-]
Certainly I don't seem to run into as many of them as I'm led to believe exists.
reply
pppppiiiiiuuuuu
11 hours ago
[-]
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.
reply
fooker
2 hours ago
[-]
reply
lovidico
8 hours ago
[-]
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).
reply
kjs3
11 hours ago
[-]
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.
reply
pjmlp
4 hours ago
[-]
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.

reply
snvzz
13 hours ago
[-]
Rust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
reply
steveklabnik
11 hours ago
[-]
… 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.

reply
fooker
1 hour ago
[-]
> Amazon even has placed bounties (and paid some) for proving things about the standard library.

Can you provide some links? Thanks.

reply