> This is not true. It has been done. I’ve seen it done for an entire OS too

That might be what pron's talking about. seL4 is only 10-20K lines of code as far as I remember. Maybe you have another OS in mind, though.