I feel like I keep saying this every single PLT-related HN thread. Sorry for preaching, but I just can't resist. I think Agda is an excellent programming language, and it's a joy to write anything in. Its learning curve is steep at the beginning but once you gain experience how to write coinfinite programs, it's such a joy.

I think its module system is a huge bonus. It makes code a lot easier to organize and reason. It forces toplevel module X to be defined in X.agda so there is no argument what the module should be named or where it should be found.