If you think that's cool, you ain't seen nothin' yet. Check out Andrew Miller's PhD thesis: a compiler that can take the Agda description of any data structure

If you think that's cool, you ain't seen nothin' yet. Check out Andrew Miller's PhD thesis: a compiler that can take the Agda description of any data structure and produce a cryptographically authenticated "Merkelized" version of it: https://github.com/amiller/generic-ads https://github.com/amiller/generic-ads Here's an implementation of a red-black tree: https://github.com/amiller/generic-ads/blob/master/RedBlack.hs https://github.com/amiller/generic-ads/blob/master/RedBlack....