Microkernel & guix

[David Craven]

Hi,

So I assume that many have already heard of the SEL4 microkernel that
contains a (~full) correctness proof (equivalence to the Haskell
functional model) and proof of various interesting properties
including confidentiality and integrity of the IPC communication and
worst case execution time for hard real time guarantees. [0]

Some other interesting developments in the OS scene is the Genode
operating system [1]. Genode is an implementation of the user-space
part of a microkernel based OS. It supports various microkernels
including the SEL4 and a handful of other microkernel implementations.
It has a driver execution environment for repurposing Linux drivers,
iPXE drivers and NetBSD drivers and provides a POSIX interface to
existing applications.

I think at some point it would be nice to start thinking about how
guix and genode could complement each other. Work is being done on
exploring how nix can help genode with it's "package management
problems" [2]. I suggest waiting to see what develops from that first.

Just thought I'd share in case someone is interested :) And make sure
that Guix devs stay on top of current developements =P

[0] https://github.com/seL4/seL4
[1] https://github.com/genodelabs/genode
[2] https://github.com/ehmry/genode-nix