The Coq mailing list

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

On 07/23/2012 12:33 PM, Paolo Herms wrote:
> 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.

Yes, I know many people disagree. :-)

I just wanted to point out that tactics are not the "uncontroversial 
right way" for writing functions with complex types.  I think direct 
Gallina programming leads to more readable and maintainable code in many 
cases, and it is worth learning the language features and tricks that 
enable such programming.

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