9

Coq is a proof assistant, while Agda/Idris are programming languages (although they can be called proof assistants).

I was exploring these languages and I wonder if Agda/Idris are sufficient to do everything that Coq can do.

So, is there some [proof/way of managing code/IDE (Emacs) functions/something else] that Coq can do while Agda/Idris can't do?

ice1000
  • 6,406
  • 4
  • 39
  • 85
  • 3
    Coq power as a programming language is similar to Agda [with main differences being pattern matching and "universes"] I am not expert on Idris but I think that both Coq and Agda have far more "logical power" than Idris. What sets Coq apart from these languages is its support for tactics, notations, extraction, and wide library support. These are very important factors in practice. Also, Coq performance, while not the best, it is robust in a practical sense. And the kernel, if you leave out modules, is reasonably small. – ejgallego Dec 16 '17 at 04:33
  • 2
    @ejgallego What about induction-recursion? Or sized types? Or a copattern-based treatment of coinductive data? Or Streicher's K? Or implicit binders? Or canonical structures? The systems are indeed pretty close one to the other but there are also most definitely important features / design choices setting them apart. – gallais Dec 16 '17 at 22:54
  • Sure @gallais, there is a reason that I didn't write a answer but a comment, and that is that writing a good answer is not an easy task. – ejgallego Dec 16 '17 at 23:16
  • 2
    Fair enough. As for Idris, there is a related SO question: https://stackoverflow.com/questions/9472488/differences-between-agda-and-idris – gallais Dec 16 '17 at 23:57

1 Answers1

7

Coq has been around for a while and has a strong community with many libraries and developments. It also has got a tactic language and some other extensions which make it very suitable for bigger projects. As far as the coq core language is concerned it often offers less than for example Agda. For example it is hard to define functions by pattern matching (even though there is an extension which helps) and it doesn't feature inductive-inductive types or mixing induction and coinduction. Most coq developments don't use dependent types (because they are difficult to use in coq) but instead use rather the combination of simply (or polymorphically typed) programs with predicates on top.

Thorsten Altenkirch
  • 519
  • 2
  • 3