I prefer agda as proof checker but its not a practical choice for building software. Lean feels like it could legitimately become a successor to Haskell as the go to functional programming language for software development.
I think what holds Agda back from being "practical" is that it just doesn't have good tactics. You can't easily automate proofs and even simplification techniques require some language-level tricks[1]. There's technically support for elaborator reflection (as in Idris) but it's painful and impossible to debug. Certainly nowhere near where Coq and Lean are.
Also true. The slowness is relatively unpredictable, too: sometimes changing a 'rewrite' to a 'with' can increase memory usage tenfold.
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.
> 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.
[1]: like this one I've used for several proofs so far: https://danilafe.com/blog/agda_expr_pattern/