24 ms·
The Lions Operating System
- cjs_ac 1y agoPresumably 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 https://en.wikipedia.org/wiki/John_Lions [1] https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Operating_System https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...
- santoshalper 1y agoIt's developed by UNSW Sydney, whose mascot is a Lion. (Specifically, "Clancy the Lion"), so I am guessing it's probably that.
- kragen 1y agoThat's also where John Lions taught.
- skavi 1y agoJohn Lions is not Lions OS is not is not Clancy the Lion
- _f9cu 1y agoWhat does mascot mean
- saithound 1y agoA 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 1y agoIt is https://www.youtube.com/watch?v=W8Ka_8kHTj4&t=903s https://www.youtube.com/watch?v=W8Ka_8kHTj4&t=903s
- woolion 1y agoThe 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 1y agoaka the Lions book
- snvzz 1y agoNot presumably, but explicitly. Both in documentation and presentations by seL4 they consistently make a point to mention so.
- spencerflem 1y agoVery cool! I’m a huge fan of Genode, another OS that runs on SeL4. Does anyone here know how they compare?
- Y_Y 1y agoUnequal
- panick21_ 1y agoGenode 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 1y ago> 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 1y agoNo, you’re totally right I phrased it badly
- hulitu 1y ago[flagged]
- qubex 1y agoThat’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 1y agoYes, 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"
- panick21_ 1y agoIts just the fastest, safest and most reliable possible operating system, giving you more formal guarantees then literally anything else ... why don't you just read more then just 1 sentence and actually spend 15min learning about the system.
- charlycst 1y agoThere is an example of interface in the docs: https://lionsos.org/docs/examples/kitty/ https://lionsos.org/docs/examples/kitty/
- kragen 1y agoThose are applications, not operating systems. With occasional exceptions, you can run any application on any operating system.
- 1y ago
- snvzz 1y agoOn 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/ https://lionsos.org/docs/examples/firewall/ 1. https://youtu.be/wP48V34lDhk https://youtu.be/wP48V34lDhk
- gethly 1y ago[flagged]
- snvzz 1y agoRust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
- steveklabnik 1y 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.
- fooker 1y ago> Amazon even has placed bounties (and paid some) for proving things about the standard library. Can you provide some links? Thanks.
- steveklabnik 1y agohttps://aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library/ https://aws.amazon.com/blogs/opensource/verify-the-safety-of...
- fooker 1y agoThis is awesome. Are these reasonably current?
- steveklabnik 1y agoThat announcement was a year ago, I haven’t kept up with the repo.
- amelius 1y agoMountain Lion is calling and wants its name back.
- CursedSilicon 1y agoYou mean OS X 10.7 Lion?
- lproven 1y ago10.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://apple.fandom.com/wiki/Mac_OS_9 https://microware.com/ https://microware.com/ Before OS 9 was OS 8, which was unrelated to OS/8. https://apple.fandom.com/wiki/Mac_OS_8 https://apple.fandom.com/wiki/Mac_OS_8 https://gunkies.org/wiki/OS/8 https://gunkies.org/wiki/OS/8 Names overlap. The hommage in this one is fairly clear, I think.
- CursedSilicon 1y agoThis is "The Lions" operating system, not "The Mountain Lions" operating system Ergo it would be 10.7 Lion, no?
- lproven 1y agoYes, that is indeed what I was getting at. I could have made it clearer by replying to the same parent comment as you. Sorry about that.
- fithisux 1y agoAussies were supposed to progress with Darbat. It never happened.
- fifticon 1y agoif you rearrange the letters, you get the Linos OS.
- pjmlp 1y agoWhile folks keep discussing C vs Rust, what got my attention was MicroPython and Pancake (https://trustworthy.systems/projects/pancake https://trustworthy.systems/projects/pancake).
- mhd 1y agoWhen 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 https://os.inf.tu-dresden.de/L4/l3elan.html
- johnisgood 1y agoI have not heard of Pancake, seems interesting. It led me to https://cakeml.org https://cakeml.org. Looking at https://github.com/CakeML/cakeml/blob/3194e00b69ce817cf477515ac309fe832eee2817/tutorial/splitwordsScript.sml#L44 https://github.com/CakeML/cakeml/blob/3194e00b69ce817cf47751..., I feel quite dumb. :P
- fithisux 1y ago"but contains composable components for creating custom operating systems that are specific to a particular task" like reviving OSfree aka 64bit OS/2
- Propelloni 1y agoIt'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.
- fithisux 1y agoOSFree is developed on top of L4.
- dctoedt 1y agoMy first thought was to wonder whether it was a Linux offshoot.
- peterisza 1y agoFinally an OS that is really an OS and not a linux distro
- mikewarot 1y ago>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.