This document outlines a plan to rewrite an operating system kernel using the C programming language with strong typing. It discusses problems that arise from using C like buffer overruns and page faults in the kernel. It proposes using techniques like algebraic data types and type classes to add flexibility without weak types. It presents existing strongly typed OSes and why they have not seen wi