> seL4 is easy to do wrong
This was our main stopper. seL4 would benefit greatly to teach how everything can be fit together, and where everything can be expected to go.
This was our main stopper. seL4 would benefit greatly to teach how everything can be fit together, and where everything can be expected to go.
Basically by providing setup, resource management, and communication abstractions that you just can't get wrong because doing something dumb that would be entirely nuts and/or would result in difficult to deal with run-time errors (as the kernel enforces some of its guarantees) ends up being rejected by the compiler ahead of time.