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