Not Unix but Lions OS[1]. Also, why would you want to build Unix on top of seL4? I think we can have better ideas than that in today's state of the art.
Thank you very much for the link, and yes you are absolutely right. I should have wrote unix'i or plan9'i or better just a universal operating-system, i meant with that not just a hypervisor but a "real/full" os on top of seL4.
And yet Unix is powering all the supercomputers, six of the seven magnificent seven, the AI revolution, nearly every single computer in all the datacenters around the world, billions of "small" devices, etc.
Can we really do that much better or is it just hubris?
At what point another approach, like the one Windows used, would be considered a failure? Once it's only powering the corporate world and not much else?
And at what point another approach would be considered a success? Once it has replaced Unix on all the supercomputers and in all the datacenters?
People like to snob Unix but the fact is: the world runs on Unix.
P.S: I wrote "Unix" with an 'i' and not a star because I have no clue how to write a star in HN's powerful text editor ; )
Linus Torvalds would have told you its system call performance, but Linux is also forced to solve these problems with things like futexes and io_uring, which carry over just as easily to microkernels.
Nowadays the excuse is side-channel attacks make any attempts at security pointless anyways so the kernel has exploded in size and complexity. This is insane logic, not least of all because side-channel attacks are read-only and can’t embed themselves into your system permanently through a bug in a browser JIT.
Linux is used purely because of all of its drivers and familiarity. Not on technical merits.
Can be prevented[0][1][2].
0. https://trustworthy.systems/publications/
1. https://trustworthy.systems/publications/papers/Sison_BMKH_2...
2. https://trustworthy.systems/publications/papers/Buckley_SWMM...
The world you are aware of runs on it.
> Can we really do that much better or is it just hubris?
Yes. Have a look at seL4[1] and Barrelfish too[2], even though that's no longer active. seL4 in particular is powering a lot of highly secure computing systems. There is a surprisingly large sphere outside of Unix/POSIX.