[HN Gopher] The Lions Operating System
___________________________________________________________________
The Lions Operating System
Author : plunderer
Score : 197 points
Date : 2025-11-20 18:19 UTC (1 days ago)
(HTM) web link (lionsos.org)
(TXT) w3m dump (lionsos.org)
| cjs_ac wrote:
| 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...
| santoshalper wrote:
| It's developed by UNSW Sydney, whose mascot is a Lion.
| (Specifically, "Clancy the Lion"), so I am guessing it's
| probably that.
| kragen wrote:
| That's also where John Lions taught.
| skavi wrote:
| John Lions is not Lions OS is not is not
| Clancy the Lion
| imvetri wrote:
| What does mascot mean
| saithound wrote:
| 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.
| mlinksva wrote:
| It is https://www.youtube.com/watch?v=W8Ka_8kHTj4&t=903s
| woolion wrote:
| 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.
| mzs wrote:
| aka the Lions book
| snvzz wrote:
| Not presumably, but explicitly. Both in documentation and
| presentations by seL4 they consistently make a point to mention
| so.
| spencerflem wrote:
| Very cool! I'm a huge fan of Genode, another OS that runs on
| SeL4. Does anyone here know how they compare?
| Y_Y wrote:
| Unequal
| panick21_ wrote:
| 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.
| lproven wrote:
| > Genode, another OS that runs on SeL4.
|
| Hang on, what? Genode can run on seL4 but seL4 is not part of
| it. Genode can also run on Linux and a bunch of other things.
| It has its own native kernel and it's not based on seL4 in any
| way, AFAIK.
| spencerflem wrote:
| No, you're totally right I phrased it badly
| hulitu wrote:
| > 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 ?
| qubex wrote:
| 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.
| lukan wrote:
| 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"
| charlycst wrote:
| There is an example of interface in the docs:
| https://lionsos.org/docs/examples/kitty/
| kragen wrote:
| Those are applications, not operating systems. With occasional
| exceptions, you can run any application on any operating
| system.
| mmooss wrote:
| 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.
| fortyseven wrote:
| Yeah, Linus, what's the point?
| lmm wrote:
| Hardly a fair comparison. Linus wanted an OS that would run
| on his own PC and let him do his Unix homework assignments.
| johnisgood wrote:
| What makes the comparison not fair? We do not know the
| author's story!
| kjs3 wrote:
| Could have been done for fun. You wouldn't understand.
| oytis wrote:
| One application would be safety and security critical real-time
| systems that also need significant amount of processing power
| vrighter wrote:
| 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
| lproven wrote:
| > What is the purpose of this OS ?
|
| What is the purpose of any OS?
|
| As all the modern ones slowly converge on similar attributes of
| being incomprehensibly vast codebases unreadable by any human,
| typically implemented in C or something closely related to it,
| using a similar underlying register-machine model, there is
| value in simply being small, simple, readable, able to do
| useful work, and being different. If something is also
| _provably correct_ that 's just the icing on the cake.
| snvzz wrote:
| 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
| gethly wrote:
| Oh no, it's written in C and not Rust. The blasphemy!
| snvzz wrote:
| Rust, an immature language with fluidly evolving specification
| / reference implementation, is not suitable for high assurance
| nor formal verification.
| steveklabnik wrote:
| ... 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.
| fooker wrote:
| > Amazon even has placed bounties (and paid some) for
| proving things about the standard library.
|
| Can you provide some links? Thanks.
| steveklabnik wrote:
| https://aws.amazon.com/blogs/opensource/verify-the-
| safety-of...
| fooker wrote:
| This is awesome.
|
| Are these reasonably current?
| steveklabnik wrote:
| That announcement was a year ago, I haven't kept up with
| the repo.
| johnisgood wrote:
| 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.
| steveklabnik wrote:
| Miri is not really a formal verification tool. It is more
| of a runtime sanitizer.
|
| And it's because Rust's "no undefined behavior" is for
| safe Rust. Miri is used dynamically at runtime to catch
| undefined behavior in the unsafe superset.
|
| Finally, Rust's safety guarantees relate to memory safety
| only. There's a lot more properties you'd want to prove
| about programs, some safety related in a broader sense,
| some totally unrelated to safety concerns.
| johnisgood wrote:
| Is it possible to find UB in "unsafe" at compile time?
| steveklabnik wrote:
| By using some proof tools, you can find some of it.
|
| It is technically impossible to find 100% of it at
| compile time because some of the finer details about what
| is UB are not nailed down 100% yet. But those are
| generally pretty fine corner cases, and one of the goals
| of those definitions is to not invalidate code as
| written.
|
| Formal verification is _very_ hard.
| aloha2436 wrote:
| 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.
| fooker wrote:
| I see you have not met a lot of Rust activists.
| aloha2436 wrote:
| Certainly I don't seem to run into as many of them as I'm
| led to believe exists.
| pppppiiiiiuuuuu wrote:
| 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.
| fooker wrote:
| https://discuss.haiku-os.org/t/replace-c-code-with-
| rust/6753
|
| https://github.com/seL4/seL4/issues/487
| aduty wrote:
| Love that discussion on the Haiku board.
| johnisgood wrote:
| Oh man, these are great.
|
| Check out https://github.com/ansuz/RIIR/issues/ for more.
|
| Gosh... and people on HN tell us that they have yet to
| meet a Rust fanatic. Just look around the GitHub Issues I
| linked.
|
| ---
|
| BTW I stumbled upon https://github.com/r9os/r9 as well.
| Reading the source code, it is mainly unsafe blocks and
| assembly. :| Who would have thought?
| adastra22 wrote:
| I am a "Rust activist" any day of the week. seL4 is awesome
| and amazing.
| johnisgood wrote:
| Thoughts on Ada / SPARK? Why are you not using Ada /
| SPARK considering it has such a neat type system, pre-
| and post-conditions, formal verification, and so forth.
| It has built-in concurrency constructs as well and it
| helps you avoid deadlocks and race conditions.
| kjs3 wrote:
| 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.
| pjmlp wrote:
| 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.
| snvzz wrote:
| Because it is not UNIX like.
|
| It does provide some degree of POSIX compatibility, but it
| does not dictate architecture.
| lovidico wrote:
| 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).
| amelius wrote:
| Mountain Lion is calling and wants its name back.
| CursedSilicon wrote:
| You mean OS X 10.7 Lion?
| lproven wrote:
| 10.8 was Mountain Lion.
|
| But before OS X was OS 9, and OS 9 was not the same thing as
| OS-9.
|
| https://apple.fandom.com/wiki/Mac_OS_9
|
| https://microware.com/
|
| Before OS 9 was OS 8, which was unrelated to OS/8.
|
| https://apple.fandom.com/wiki/Mac_OS_8
|
| https://gunkies.org/wiki/OS/8
|
| Names overlap. The hommage in this one is fairly clear, I
| think.
| fithisux wrote:
| Aussies were supposed to progress with Darbat.
|
| It never happened.
| fifticon wrote:
| if you rearrange the letters, you get the Linos OS.
| pjmlp wrote:
| While folks keep discussing C vs Rust, what got my attention was
| MicroPython and Pancake
| (https://trustworthy.systems/projects/pancake).
| mhd wrote:
| 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
| pjmlp wrote:
| Cool, thanks for the link.
| bolangi wrote:
| For a short while, I ran the Eumel operating system and wrote
| an application in Elan. Among other interesting properties,
| files weren't saved, but were checkpointed by the OS. I
| enjoyed this exercise, although Eumel remained a very small
| niche.
| johnisgood wrote:
| I have not heard of Pancake, seems interesting. It led me to
| https://cakeml.org. Looking at https://github.com/CakeML/cakeml
| /blob/3194e00b69ce817cf47751..., I feel quite dumb. :P
| fithisux wrote:
| "but contains composable components for creating custom operating
| systems that are specific to a particular task"
|
| like reviving OSfree aka 64bit OS/2
| Propelloni wrote:
| 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.
| dctoedt wrote:
| My first thought was to wonder whether it was a Linux offshoot.
| peterisza wrote:
| Finally an OS that is really an OS and not a linux distro
| mikewarot wrote:
| >It 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.
|
| Unfortunately, like Genode, this approach yields something that
| is interesting, but can't be a daily driver for me. 8(
|
| Meanwhile, the US national security continues its downhill slide
| because we've chosen operating systems based on ambient
| authority.
___________________________________________________________________
(page generated 2025-11-21 23:02 UTC)