I think it's poor methodology combined with a "dangerous" language: lack of unit-testing/TDD, low-level verbosity, lack of formal behavior prooofs, kitchen-sink

I think it's poor methodology combined with a "dangerous" language: lack of unit-testing/TDD, low-level verbosity, lack of formal behavior prooofs, kitchen-sink features lumped into the kernel, constantly reinventing the wheel and lack of minimal package code re-use. Don't get me wrong, I learned all the sharp edges by trial-and-error in the C89 days with Pascal and embedded assembly, but I think we've got to have systems languages which provide higher-level abstraction for bare-metal kernels. It's just that even codebases like OpenBSD don't go far enough like seL4 to verify their security model beyond reasonable doubt with formal methods.