Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by tom_mellior on Wednesday August 07, 2019 @12:04PM (#20635952)

* shrug* Coq users have the choice between using tactics and writing proof terms like Agda users. 99.9% of Coq users choose tactics 99.9% of the time. They might know something you don't know, or you might know something they don't know. You decide.

I'm not going to argue about a paper written by someone whose proficiency in Coq I cannot judge with someone who doesn't seem to know anything about Coq except having read this one paper.

F* looks very good in this comparison, which is great. As you wrote above, we need better tools, and F* is getting there. Simple things can be tedious in Coq, and F* 's automation should help there.

[ Parent | on HN ]

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Blaisorblade0 on Sunday August 11, 2019 @07:01AM (#20667556)

Having used both, Coq proof terms aren't Agda proof terms. Coq provides neither "real" dependent pattern matching nor edit-time tactics. Long-term, the vision in Agda would be to support metaprogramming closer to what you do in FP languages. But even now, there are domains where Agda is competitive (tho they seem to be in mechanizing mathematical theories, as in, things designed by mathematicians to be compact). To prove software correct, you'll likely end up with with proofs you'll want to automate.

Regarding compatibility: neither Coq nor Agda used to have much of it; nowadays Coq is maintained together with a large set of community projects, and code is much more stable. Still tons to do.

[ Parent | on HN ]