> sel4 is very limited in scope and extending that to a semi-usable OS (that uses ""proven"" C) is expensive time and money wise.
Everything that has to meet a high criteria of safety is like this, yes. For the exact same reason unsafe exists in Rust and completely inescapable, because automatic correctness checking beyond the most trivial static analysis doesn't actually come for free, and it imposes intense design restrictions that make a lot of things very time consuming to do.
You will never find a single point in the multiple archives of Linux's git history where a clean break point occurred and the kernel was greenfielded with the express intent of replacing its design abstractions with ones more appropriate and ergonomic for formal analysis. If you'd like to express further skepticism, feel free to try and find that moment which never happened.
Participation of large, well recognized corporations does not imply the kernel isn't a mess of technical debt. It actually implies worse.
Everything that has to meet a high criteria of safety is like this, yes. For the exact same reason unsafe exists in Rust and completely inescapable, because automatic correctness checking beyond the most trivial static analysis doesn't actually come for free, and it imposes intense design restrictions that make a lot of things very time consuming to do.
> Citation needed
https://groups.google.com/g/comp.os.minix/c/dlNtH7RRrGA/m/Sw...
You will never find a single point in the multiple archives of Linux's git history where a clean break point occurred and the kernel was greenfielded with the express intent of replacing its design abstractions with ones more appropriate and ergonomic for formal analysis. If you'd like to express further skepticism, feel free to try and find that moment which never happened.
Participation of large, well recognized corporations does not imply the kernel isn't a mess of technical debt. It actually implies worse.