I'm not familiar with SeL4 other than in the abstract sense that I know it's a verified kernel.

I interpreted your statement "Then also allow the kernel to run linux as a process, and run whatever you like there, however you want." as the Linux process being analogous to a VM. Invoking an emulator wasn't really the right analogy. Sorry about that.

For me it comes down to this:

As long as the root-of-trust in the device is controlled by the device owner the copyright cartels, control-freak developers, companies who profit end users viewing ads, and interests who would create "security" by removing user freedom (to get out of fraud liability) won't be satisfied.

Likewise, if that root-of-trust in the device isn't controlled by the device owner then they're not really the device owner.

Yes; I think that's the real impasse here. As I say, I think there is a middle ground where the device owners keep the keys, but programmers can run whatever software they want within sandboxes - including linux. And sandboxes aren't just "an app". They could also nest, and contain 3rd party app stores and whatever wild stuff people want to make.

But a design like this might please nobody. Apple doesn't want 3rd party app stores. Or really hackers to do anything they don't approve of. And hackers want actual root.