Large systems need to be able to update seL4 and libsel4 without recompiling the rest of their userlands. I had considered embedding libsel4 into the kernel binary itself, but a better approach would be for libsel4 to be linked into the root task, and for the process-creation routines to map libsel4 into every address space they create. Ideally, there would be only one copy of libsel4, just like their is only one copy of the kernel.
Right, as the kernel isn’t actually responsible for loading images, whatever user-level task is responsible for loading images would be responsible for ensuring that. This would be fairly similar to VMS, WinNT, and Linux’s VDSO mechanism. In this case, you’d be relying on a stable C ABI with a stable libsel4 API on top.
The downside to this approach is that you introduce a large number of indirect branches (potentially via function pointers) where you could otherwise inline the fairly small system call invocations. It would probably be preferable to provide a higher-level OS interface in this manner that uses the inlined versions of the seL4 API (and is thus tied to a specific minor version of the kernel) but is itself loaded in the manner you are speaking.