Liam,

The reason I keep coming back to this is the complexity of modern OS 
threats and requirements and the desire to spend less of my time here.

The core drivers of the seL4 API are (from 
https://microkerneldude.wordpress.com/ ; good reads here BTW):

Verification
------------
-Minimality  [* Small _IS_ beautiful ! *]
-Policy freedom
-Performance
-Security
-Don’t pay for what you don’t use

Then there are a few non-goals:
------------------------------
-Stopping you from shooting yourself in the foot [*systems programmers 
have to aim through their heads;^]
-Ease of use  [*we can help here*]
-Hardware abstraction [*we should be able to help here*]

So starting with a minimalist open source microkernel running drivers, 
servers, apps as hot swapable Smqlltalk runtime components in separate 
user-land address spaces with _fast_ IPC makes sense to me as a 
strategy.

If the systems architecture is right and there is enough interest, we 
can drill down to the bottom level, but in the mean time we can devise 
and experiment without getting bogged down learning the details of tying 
our shoelaces before the big race.

My thought is to have a copy-on-write core (I am thinking again or 
something like the Bee DMR binary core here) with a system naming 
service that is used to intern all selectors, so IPC uses common 
selector keys.  Capabilities map to Smalltalk objects in their home 
address spaces (note 
http://mumble.net/~jar/pubs/secureos/secureos.html).

So code+component(s) = driver or service with core just copy-on-write 
(with resilient live update).

I would think that all of this maps into (perhaps grad level) student 
projects as well, so [a] we can get a bit of "free labor" boost plus [b] 
more beginning and advanced students get exposed to Smalltalk and the 
ideas of the community.

$0.02,
-KenD