SafeHouse: an experiment

• (1) Start with a minimal compiler and run-time system
  • There is hope that critical properties can be verified formally
  • Grow it without sacrificing formal verification
• (2) Make use of dependent types
  • More safety constraints can be captured as type-safety
    • Fewer bugs!
  • More safety checks can be moved from run-time to compile-time
    • Potential for better performance!