And yet at some complexity level you have things like ARINC 653 where the usual implementation is to have a classic RTOS running on each of the partitions provided by the "application executive", and today's serverland is hypervisors running VMs running containers. I believe we are too centered on the "Linux vs Minix" debate while in actual practice both tendencies are reflected in most systems.

>RTOSes are used and not fully fledged OSes.

The idea that "RTOS" and "fully fledged OS" are incompatible with each other is outdated.

seL4 advanced the state of the art with its formally-verified support for mixed criticality, years ago already.

There’s actually a real-time microkernel that millions of children use daily. It’s called the Nintendo Switch.

(But seriously, it’s a homegrown microkernel RTOS.)

The idea might be outdated, but as I have yet to seen a system running seL4, in practice it is very much true still.