I suppose it depends on what you include in the kernel. Our OS framework is a set of cooperating services, but the great majority of that is app code with no particular privileges – things like a math library, but including a lot that in legacy CPUs has to run in the kernel.
We define the real kernel as that code which has to be trusted because it can unilaterally change the state and condition of other code that is not trusted. This trust is different from code that is relied upon: if your app uses sqrt in some calculation, you rely on the math library to in fact give you a square root. But sqrt cannot change the state of its caller (courtesy the Mill protection model) so the app does not have to trust it in this sense.
So what has to be trusted? Not very much on a Mill: some initialization code for boot; the top-level interrupt handler; the dispatcher; a few allocators; and most importantly, the code that updates the protection state. We project ~3k LOC total. And nearly all of that code exists to deal with the way the Mill works, so it can’t be shared with any other platform, in either direction.
Of course, surrounding that microkernel there will be a ton of untrusted (but relied upon) libraries that we expect to lift from L4 and anywhere else. That will include a lot of what the original source thought was part of the kernel, but we don’t.
We anticipate considerable terminological confusion.