As you’d expect, this involves creating a monad for all the actual messy OS stuff. The capabilities therein are described by quite nice type classes (potentiall

As you’d expect, this involves creating a monad for all the actual messy OS stuff. The capabilities therein are described by quite nice type classes (potentially representing hardware capabilities or your own address space, for example), which is interesting because you could build something like OpenBSD’s pledge that’s formally provable at the type level etc. I remember another somewhat functional approach to OS programming being to hide the privileged bits of system calls behind curried functions so your process gets effectively a private view of the kernel: http://4e.iwp9.org/papers/usecsys.pdf http://4e.iwp9.org/papers/usecsys.pdf All very much over my head, of course, but always interesting to see paradigms prove robust all the way up and down the software stack.