Do more of the current H monad interface.
Make more complex memory access patterns safe:
Manipulating linked data structures.
Safe DMA programming.
A dependently typed H monad (sketchy)?
type H M
a peek ∈ (a∈Addr) → H M M (M a) poke ∈ (a∈Addr) → T → H M M[a→T] ()
Separation properties in the types?
Verifying the compiler and run-time system properties. (Use ideas from ?)