I've been using almost nothing else than Debian GNU/Linux on i386 and amd64 PCs, since 1992. (I helped birth Linux, and I was part of Debian for a long time.) I have been happy for myself, but speaking more generally, I think it'd be awesome, nay, AWESOME, if computing wasn't so homogeneous. Almost everyone is using Windows or Mac. Outside that, it's mostly Linux, with a few BSD variants. I hope to see that change, some day.
Ideally, radically different, not just another Unix.
However, having lived through the entire lifetime of Linux, it's not easy to develop an entire operating system, and its supporting ecosystem, if you need it to be usable with current and near-future hardware and common devices without extensive effort to set up and configure by users.
Copying drivers means copying some of the software architecture and bugs, too. Less heterogeneous.
(Just idly ranting, waiting for a test run to finish.)
@liw I completely agree both that it's desirable to have new experimental OSes flourish, and that the biggest barrier is hardware support.
I have this hypothesis that there's a vaguely formal-methods shaped way to describe the behavior of hardware independent of the behavior of any particular OS, then mechanically validate OS-specific drivers against those models. In that world, the models could be shared across operating systems, rather than the drivers themselves.
People would still need to write drivers for each new OS, but if you know how the hardware behaves, there are usually not many choices for what the driver can legally do at any given time. Tooling could help guide the driver writer through those choices.
My imagination here is mostly inspired by Termite 2 (https://trustworthy.systems/publications/nictaabstracts/Ryzhyk_WKLRSV_14.abstract). I also once attempted to replicate the original Termite work (https://github.com/jameysharp/lotos/), which didn't work out for several good reasons, but I wrote up a lot more thoughts about this there.
@jamey @liw I would love for this to work, but "if you know how the hardware behaves" is quite a big If. Hardware is also quite buggy, and sometimes those bugs are hard to characterise.
Still, if the model can properly represent all the bugs, I can imagine this would help to share the knowledge across multiple OSes.
@bwh @liw Oh, this is well into "open research question" territory, so that's the smallest of the big Ifs, honestly. Formal methods are of course only as good as the models driving them. But we write drivers based on incomplete information all the time, and this imaginary tooling wouldn't change that. We'd be writing down our beliefs about how the hardware works, rather than describing objective reality.
But I still believe that would be a huge improvement, because then we could talk about those beliefs in a common framework, without OS details getting in the way. And when somebody identifies a correction to some model, every driver using that model could be mechanically re-verified.
If you want to list the bigger challenges to my thought experiment, there are plenty. Like how hard it is to devise a modeling framework that allows us to express the wide variety of things hardware can do, while still being restricted enough that it's possible to mechanically prove that a driver is correct with respect to its model. Or how much trouble it is to do anything mechanically with C source code; my old C-to-Rust translator, Corrode, suffered from that problem too.
Nobody yet knows how to build what I'm describing. I just think it's a vision worth investigating, especially as an alternative to trying to make driver source code for one OS build on another.
Lars Wirzenius
Jamey Sharp
Ben Hutchings