[tomsmeding]

My experience with this kind of stuff: done some Coq by myself and some HOL in class.

Generally, the distinguishing feature of tactics is that they provide backward reasoning, instead of forward reasoning, what a verification engine would be written around. Mind that I haven't worked with any proof system yet besides Coq and HOL, so my opinion might be far out, but I think backward reasoning is a very nice way to construct proofs, especially in the context of a proof assistant.

Aren't things like algorithms for simple automated proving more easily embedded in a tactic language than in a forward reasoning language? When reasoning backward, one naturally reduces the statement to prove to simpler and simpler statements, and at some point they become simple enough to be handled by some automatic prover. (auto/omega/... in Coq, PROVE_TAC/COOPER_TAC in HOL) When reasoning forward, I don't see how one would go about using automated provers like that, but it's likely I'm missing some idea here.

> I'm currently writing my own dependently typed PL

Awesome! I'm all for writing interesting new languages and implementations, especially in this area. Once you've got something to show, be sure to post here on HN, since people might enjoy looking around. :) (If it doesn't get lost in the swarm of submissions...)

[gnulinux]

I think forward reasoning works only because the underlying type theory is intuitive. When I approach proofs in agda, I simply approach it the same way I write haskell code. "You have bunch of cosets and you wanna go to group." You have objects (proofs) around and you want to construct an instance of a type (theorem) so you start with functions (lemmas) that give objects of desired types. Again, I'm not very familiar with Coq (only agda) but I suppose by backwards reasoning you mean the last unconstructed type in your proof is the type with highest level of abstraction. On the other hand, in agda it's the first one because either you already know a function (lemma) returning this type and need to construct it's arguments (assumptions) or you can use an anonymous function (implication introduction).

This is a totally random and not a well-thought-out statement but to me it seems like the difference between agda and Coq seems like the difference between purely functional and imperative programming.

[tomsmeding]

I think I just need to try out something like Agda before I make any more claims :) Does Agda have something that can automatically prove small formulas in e.g. pure predicate logic?

Backwards reasoning works something like this: to prove 'forall n: P n', it is sufficient to prove 'P 0' and 'P n => P (succ n)', so if you have 'forall n: P n' as your so-called proof goal, you can use the induction tactic to transform that into two goals: 'P 0' and 'P n => P (succ n)'. You then have to separately prove both goals. The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.

> the difference between agda and Coq seems like the difference between purely functional and imperative programming.

Bold, bold :) I'll have to try Agda before I can comment on that. Coq proofs do seem a bit inperative, so there's that.

[TezlaOil]

> The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.

In Agda, you would type something like `nat-ind ?x ?y` into a hole of type (forall m -> P m). Then ?x becomes a hole of type (P zero) and ?y becomes a hole of type (forall n -> P n -> P (suc n)), and you can fill these holes with proofs at your own leisure. It does not feel all that different from using `induction m` in Coq. In Agda, you'd normally implement your "reflective tactics" as functions, or you'd write macros if you really need them (e.g. for ring solvers), but there is no separate tactic language and proofs are never tactic scripts.

[uryga]

> the underlying type theory is intuitive

isn't that "intuitionistic"?

[gnulinux]

No I meant intuitive like easy to understand for humans. (It is also intuitionistic but that's a technical fact shared by both Coq and Agda (though not HOL)). The reason I said that is because thinking in terms of types is very straightforward for people. "Give me a View and Serializer so I can give you JSON" "Why is my code not working? Oh because you can't always find the head of a list, I need to give you NonEmpty List T". Similarly, proving something is a group is like trying to go Group somehow from the objects around.

[uryga]

ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )