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.

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"

Its 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.

There is an example of interface in the docs: https://lionsos.org/docs/examples/kitty/

Those are applications, not operating systems. With occasional exceptions, you can run any application on any operating system.

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.

Yeah, Linus, what's the point?

Hardly a fair comparison. Linus wanted an OS that would run on his own PC and let him do his Unix homework assignments.

What makes the comparison not fair? We do not know the author's story!

Could have been done for fun. You wouldn't understand.

One application would be safety and security critical real-time systems that also need significant amount of processing power

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

> 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.

The primary focus of Lions/seL4 is security, and formal verification of it. It's a necessary project for a world where CVEs are frequently published for the Kernel and other underlying system services, in part because they're still using a 1970s OS design which didn't have internet-connected computers in mind.

The seL4 kernel uses an Object-Capability system (ironically which have also been around since the '70s) in place of Access Control Lists used in POSIX systems. The idea behind capabilities is "don't separate designation from authority" - the capability is both a designator of a resource and the authority to use it - there are no separate ACLs. Separation of designation from authority leads to confused deputies - where one process with lower privileges can trick a higher-privileged process to use the higher privileges on its behalf, which very often leads to privilege escalation vulnerabilities (ie, RCE as root).

Each process has a "cspace" (Capability Space), which holds the capabilities the process may use. When the process performs a system call, it references a capability slot from a set of tables in its own cspace where the capability is held, and the Kernel verifies that the capability is valid in order to perform the syscall. The capabilities can be revoked at any time, and importantly, they cannot be forged - only delegated.

Additionally, seL4 is a microkernel design which is intended to have a small attack surface. It provides only a small number of system calls like `Send`, `Recv`, `Yield`, and combinations of, such as `Call`, `Reply`, `ReplyRecv`. It's a generic interface where an IPC buffer is passed along with a set of delegated capabilities, but there's no specific calls such as `SYS_write` or `SYS_mmap` - these are built on top of the `Send`/`Recv` syscalls and their services are provided by other user-space daemon processes.

One of the best developments of seL4 is the "Mixed-criticality system" support, which provides capabilities for processing time - to enable some processes to have real-time support without becoming CPU hogs.

seL4 can also be seen as a hypervisor which can virtualize other kernels, and part of the Lions effort is to be able to utilize Linux drivers using isolated Linux guests.

To learn more, the seL4 manual is a good place to start: https://sel4.systems/Info/Docs/seL4-manual-latest.pdf. There's some videos on Youtube by Gernot Heiser discussing the MCS support.