4 ms·
> 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 expec
by mmrezaie 7y ago
> 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.
- im_down_w_otp 7y agoWe overcame this with a significant amount of Rust-i-ness and effort in understanding the guts of the kernel and how it implements its assurances. 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.
- repolfx 7y agoWhat sort of mistakes were easy to make?