The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Victor Porton wrote:
> Probably a stupid question:
>
> Why Coq has special language for writing new tactics, while Coq proofs can be 
> turn into programs? Can't programs generated from existence proof be use 
> instead of tactic scripts?
>    

You seem to be mixing two questions:
1) Why have Ltac when we also have Gallina, in which dependently typed 
functions that find proofs can be written?
2) Why not produce such functions by extracting from constructive proofs?

For the second question, I'll just say that hardly anyone anywhere, 
using any system, extracts programs from proofs.  It just isn't that 
useful of an idea, though it sounds nice in theory.

For the first one, I invite you to try doing all your proofs directly as 
Gallina terms.  I usually argue against dynamic typing, but I really 
like it in Ltac, because every program exists only to generate a proof 
term, and we can check those statically after the fact.  You would need 
quite complex typing to support the proof manipulations that are natural 
in Ltac.  Also, it would be harder to integrate good error messages and 
other tool support with Gallina tactics.