[tom_mellior]

> Coq with tactics does not fair particularly well on anything more than toy examples

Actual citation from the paper or some other source needed.

Relevant-ish citations from the paper:

1. "Coq uses interactive tactics to prove goals, which is veryconvenient, but may lead to large proof scripts in case onedoes ad-hoc proofs. But Coq also has the tools to make theproofs concise, provided one works in a fixed domain, andcreates the necessary abstractions."

2. "In [50] Wadler states“Proofs in Coq require an interactiveenvironment to be understood, while proofs in Agda canbe read on the page.”, while this is true for the languagesthemselves, but Proviola [49] can alleviate this problem ofCoq, by recording the proof state after each tactic execution,and producing an html document with the proof state addedfor each tactic. F* does not have this problem, as the proofterms do not appear either in the source, or during proving.Whether it is easier to read complete proof terms, or thereplay of a step by step creation of a proof term is dependentof the task at hand, but the author thinks, that it is morestraightforward to create scripts step by step in Coq, thoughit does require discipline on the programmer’s part, so as tonot create a write-only script"

Are you basing your very wide claim on one of these that don't say what you're saying, or did I overlook one?

Anyway, there's CompCert (http://compcert.inria.fr/) and Iris (https://iris-project.org/) and Kami (http://plv.csail.mit.edu/kami/papers/icfp17.pdf) and many other projects of non-toy size implemented in Coq, so I don't quite know what else to say to convince you. Sure, tactic scripts can be hard to read and next to impossible to skim. The same goes for direct proof terms.

> Better tools are still needed

Agreed.

[naasking]

Take a look at how much trouble the author had finding a working ST, despite there being widely published and used libraries at some point but which no longer work in newer versions of Coq. The author ended up using a very specific git hash version of the Iris library, and he admits the documentation of Iris is pretty much non-existent.

This doesn't inspire confidence, considering this author is also the most familiar with Coq of the three. He also somehow claims that Coq is stable, which I can only take to mean that it won't crash rather than that it largely preserves backwards compatibility given his difficulties. If we can't rely on some measure of backwards compatibility so we can build on stable libraries, theorem proving simple won't scale any more than programming of any kind won't scale in the same circumstances.

The number of lines of code required for the second task also doesn't inspire confidence that theorem proving with Coq will scale.

So I frankly can't see any reason to think that Coq even with tactics is a viable approach to real world verification beyond exploratory toy examples. No doubt we have different goals in mind when it comes to verification/theorem proving, which is why you think Coq is suitable and I do not.

[tom_mellior]

* 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.

[Blaisorblade0]

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.

[logicchains]

If you doubt the usefulness of tactics, check out any of Adam Chlipala's papers, like http://adam.chlipala.net/papers/BedrockICFP13/.

[naasking]

I'm very familiar with Adam's work. Now consider that he did a lot of work on Ynot, and as per this paper, Ynot no longer works with latest Coq.

The question is not whether tactics are useful in some cases, the question how robust and stable they are, because if older libraries employing tactics no longer work, this is not a robust foundation for long-term verification efforts.