[HN Gopher] A functional approach to memory-safe operating systems
       ___________________________________________________________________
        
       A functional approach to memory-safe operating systems
        
       Author : luu
       Score  : 20 points
       Date   : 2023-01-03 09:10 UTC (13 hours ago)
        
 (HTM) web link (pdxscholar.library.pdx.edu)
 (TXT) w3m dump (pdxscholar.library.pdx.edu)
        
       | thom wrote:
       | 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
       | 
       | 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.
        
       | anfelor wrote:
       | This should have an (2011) in the title.
       | 
       | luu, could you say a few words on what you found interesting
       | about this thesis? The first chapter sounds impressive, but later
       | it only seems to be defining a monad around typical operating
       | system tasks. That means you still have to deal with GC, and I
       | would not call that approach "well integrated with purely
       | functional programming", as it essentially defines an imperative
       | DSL. But I have only looked at this briefly and I would
       | appreciate deeper insight.
        
       | mike_hearn wrote:
       | Related efforts:
       | 
       | https://www.microsoft.com/en-us/research/project/singularity...
       | 
       | https://en.wikipedia.org/wiki/Midori_(operating_system)
       | 
       | http://jnode.ro/
       | 
       | None are functional but as noted in other comments, you end up
       | needing to do everything in a monad anyway if you try to do an OS
       | in an FP language. An OS is all about managing a large and
       | fundamentally imperative block of hardware state so pure FP isn't
       | an obvious fit.
        
         | weatherlight wrote:
         | MirageOS is an OS built in a (mostly) FP language, Ocaml.
        
       ___________________________________________________________________
       (page generated 2023-01-03 23:00 UTC)