I'm using Agda for my master's thesis in type theory and my god. I thought Haskell was a language with some insane design decisions due to being written by academics, but Agda really blows it out of the water. Who makes a language with untypable unicode characters as obligatory parts of the syntax?? I've had to hold my nose and install Emacs.