Hacker News new | ask | show | jobs
by kramerger 1470 days ago
> It exists to brag about verification

That is pretty much my own experience with sel4. Not very useful for real world
1 comments
senko 1470 days ago
That's interesting, do you think the poor DX is due to not enough effort being made to make it more useful for outside devs, or because making it possible to do verification makes other things ugly and inconvenient?

I was considering seL4 for a hobby project (having worked with L4Ka:Pistachio a long time ago), but didn't dig deep enough to spot these problems.

link
kramerger 1470 days ago
The latter, in the sense that it has been scaled down significantly to make verification possible.

As soon as you start adding stuff or running it in a different hardware the verification will no longer apply, so why bother?

link