The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

On Monday 23 July 2012 17:57:34 Adam Chlipala wrote:
>  I really advise not using tactics to build dependently typed 
> definitions with computational content.

I don't agree in this. If you carefully program your tactics, then they can 
be 
guided by the dependent type to be produced. 
For instance, in Wolfram's example [a] is the only value that will allow to 
prove the output type.
In bigger examples, where the tactics could produce more than one instance, 
you could terminate the proof with [Defined] and then show some properties 
about the definition, like minimality or whatever.
So quite the contrary: Dependently typed definitions are precisely the only 
ones with computational content you could build using tactics.
I think tactics can be powerful and certified code generators.
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France