Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS.
It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed.
I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.
I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.
tombert|3 months ago
It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed.
I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.
AlotOfReading|3 months ago