Agda is well-suited to computing with values that carry around various formally-checked properties. That's useful to some people for some tasks. If it's not suited to whatever you're doing, then don't use it; I presume your projects don't all use Java, Bash, Prolog, Python, COBOL, Pure, Unlambda and MATLAB at the same time; well, just add Agda to that list.
> _Agda is a programming language_
Well, that's because programming languages and formal systems (proof languages) are the same thing ( http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond... ).
Agda is well-suited to computing with values that carry around various formally-checked properties. That's useful to some people for some tasks. If it's not suited to whatever you're doing, then don't use it; I presume your projects don't all use Java, Bash, Prolog, Python, COBOL, Pure, Unlambda and MATLAB at the same time; well, just add Agda to that list.