[vacuity]

I think I've got the gist now. Although I think Gernot Heiser doesn't consider the following to be ideal, I think it's fair to say that true claims have undergone some sensationalization. I don't think people generally lie when they say their product has achieved some impressive performance, but those results exist in the context they are taken under. In the embedded roles LionsOS is being targeted for, I have no doubt that they represent a real improvement over existing Linux systems, and probably any Linux system short of a magical one. However, in a general-purpose OS (which is what I focus on), which is the same as saying that many distinct user bases are simultaneously involved, the kernel is far from being the only load-bearing component. Also note that the functionality compared is not 1:1, nor is Linux the final contender of monolithic systems.

Something I want to explore, and which has some viability in the LionsOS model too, is that a general-purpose system may still liberally cut out unused functionality if highly modular and easily configurable. Like Legos.

In conclusion, props to the people at Trustworthy Systems as always, but it's safe to say that the OS field is still far from settled. My best compliment to seL4 is that it has raised the bar and simultaneously paved the way for future generations of advances. It's a seminal work that was desperately needed.