1. 13
    1. 8

      Nobody uses Hurd because there are no killer features in it. There’s no reason to be interested in it over other microkernel systems. It’s stuck in the 90’s, and has let three major revolutions of computing technology go by completely unnoticed. It has never pushed the state of the art, it has never added to a useful ecosystem, and it has never had anyone take it and make a useful technology out of it. L4 and other microkernels can definitely be turned to useful purposes, but when was the last time anyone EVER said “You should check out Hurd because you can do X and it’s great, let me show you how cool it is”? Never that I’ve seen. People say this for Plan 9, for MacOS, for Linux, for various BSD’s, for Illumos, and for Windows. Even Minix has a couple killer applications. Hurd? None that I’ve ever seen.

      Kill it, take the useful parts (if any), and build something new with it that has an actual goal and motivation.

      1. 2

        You’re completely right. But at this point I fully expect Hurd to be something I hear about every few months for the rest of my life, and that’s somehow strangely almost comforting.

    2. 3

      Because seL4 is the only known OS that can full pass the formal verification (so far, full passed for ARM, x86 is still not full passed). seL4 is so extrodinary that …

      That sounds copy-pasted from the marketing material seL4 is pushing at the pentagon. Even if seL4 was formally verified its still just an embedded RTOS kernel that is unsuitable for general purpose systems. Driving a weapon is not the same as driving a laptop.

      If you want some formal verifcation to drool over, see Muen, it’s actually used in production: https://muen.sk/

      1. 1

        I enjoyed the first part providing the historical background. But I skimmed through the rest after I reached.

        Now let’s back to seL4.

        First, it’s GPLv2, not as good as GPLv3 but still very good in my opinion.