[ashafer]

As someone who worked with seL4, it's because the development experience is literally the worst you can possible have. It's zero fun and anyone who has to deal with it inevitably ends up hating seL4. It exists to brag about verification, developing real applications on it is a fool's errand.

[kramerger]

> It exists to brag about verification

That is pretty much my own experience with sel4. Not very useful for real world

[senko]

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.

[kramerger]

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?

[dale_glass]

That's interesting, could you provide more details? What are the un-fun bits? Too restricted? Too slow? Too hard to debug the application?