What makes that a 'language' and not just a program? When I create a 'GameBoard' class in an OO language, I don't tell someone I created a new language.
Doesn't a language have to be turing complete to be a language?
I haven't used any of these, but my understanding is that Agda and Coq are not Turing-complete, nor is Idris with the totality checker on. Never seen anyone dispute these being referred to as "languages."
Doesn't a language have to be turing complete to be a language?