House Today (1)

Uses GHC (the Glasgow Haskell Compiler)

• The compiler is big!
• The run-time system is big!
  • If we are implementing a micro-kernel in Haskell, this will be the biggest part.
• Can it be trusted?
• Can critical properties be verified formally?