This paper presents our vision and work in progress on deploying a high-level functional language with a rich and accessible type system for better modelling and verifying systems programs.