This is sooo coool :o

Simplicity with which this tool allows you to define optimization is impressive on its own (example) (optimizations are known for being hard to write), but this also allows you to do analysis (like formal verification)?? So cool!!

Also, it's nice to see the idea of "pattern is the inverse of constructor" — something I was meaning to put into a blog post for the longest time.