House and the H(ardware) monad, demonstrates that using a high-level, type-safe language like Haskell allows us to create a clean API for programming operating system kernels in a safe way. By describing the semantics of the API formally, it becomes possible to formally verify that code written on top of the API satisfy desirable properties, such as security requirements.
But there are weak spots in the approach we have used so far:
This talk describes a small experiment aimed at overcoming the above weak spots: we use dependent types to capture all safety constraints in the type system, eliminating the need for run-time checks, and we use a compiler and run-time system that are two orders of magnite smaller than GHC. We set up a small example that accesses screen buffer memory to display a text message on the screen in safe way.