The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

On Fri, 20 Feb 2009 08:39:06 -0500
Adam Chlipala 
<adamc AT hcoop.net>
 wrote:
> On the issue of proofs, I think the proof scripts in both your (Adam 
> Koprowski's) code and the code of the mysterious "muad" are manual 
> enough that I would refuse to accept them in a serious
> development. ;-) I say that every certified function should have a
> single proof script associated with it, and that proof script should
> be a single tactic, with no intermediate periods.  That style (which
> I used in my implementation posted earlier) is easy to use when you
> commit to following it, and it has many advantages in brevity of code
> and resilience to changes in specs and implementations.

But any proof can be turned into a tactic, whose definition is simply
the original proof - but that would achieve nothing. What is the formal
definition of what you mean? ;-)
-- 
Robin