> While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that.

lmao i've been there. Agda is my first choice for proof checker and for math-y explorations but its not gonna be a replacement for Haskell as a production programming language.