View Single Post
  #6   (View Single Post)  
Old 11th January 2017
gpatrick gpatrick is offline
Spam Deminer
Join Date: Nov 2009
Posts: 226

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.
Reply With Quote