Playing with authenticated data structures
Started with http://www.cs.umd.edu/~mwh/papers/gpads.pdf and seeing what falls out in Idris 2.
Playing with this definitely led me in the direction of Authenticated computations as a library, which uses monad composition. Getting things to scale how I want them to within the Idris 2 type system has remained an interesting challenge.