> I know Agda isn't really a programming language, but then why is this book trying to claim it is? It says at the start: > _Agda is a programming language_ W

> I know Agda isn't really a programming language, but then why is this book trying to claim it is? It says at the start: > _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_correspondence 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.