Quote:
Consider the size of the "proof" that would be required. seL4 is a micro kernel. Just a kernel, consisting of 1100 files, with 95,000 lines of code.
OpenBSD is a complete operating system. That system consists of:
|
Plan 9 is a complete operating system and the kernel is only 150,000+ lines of code. Add in a few thousand more for libs, userland and such, but it is still rather small.