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
- More safety checks can be moved from run-time to compile-time
- Potential for better performance!