This is really interesting work. Dependent types are fascinating but they seem so resolutely stuck in academia; evidence of applications to real-world problems is rare.