News for hackers. Stuff that matters.

A comment on The Helios microkernel. Parent comment

Re:The Helios microkernel by senko on Thursday June 16, 2022 @12:57PM (#31768349)
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.

[ Parent | on HN ]
Re:The Helios microkernel by kramerger on Thursday June 16, 2022 @02:20PM (#31769246)
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?

[ Parent | on HN ]