Peek and Poke with Dependent Types

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:

1. We compile our programs with GHC. Can we trust that GHC and its run-time system is correct? If our goal is to implement a high-assurance micro-kernel in Haskell, at least 90% of the code in the resulting system will come from the GHC run-time system, which is implemented in C and is bigger than a monolithic BSD kernel.
2. Even though type safety in Haskell allows many safety constraints to be verified at compile-time, certain checks are left until run-time, delaying bug detection and slowing down the resulting code.

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.