I am excited for this. I haven't read it all yet, but what I have has been interesting, and I look forward to reading the rest.
Maybe this will be what I will use to get myself to finally learn idris.
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.