The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

On Sun, 22 Feb 2009 12:42:18 -0500
Adam Chlipala 
<adamc AT hcoop.net>
 wrote:

> If you want to reason about your (transparent) definitions after you 
> finish writing them, then [refine] is likely to be much more helpful 
> than [Program].  The latter will add all sorts of coercions "behind
> the scenes."

Yes, which can make Programs more concise. I find this helpful.

>  The program you write will in general not be the
> Gallina term that you end up with, and it's that Gallina term that
> you'd need to prove things about.

True, but so what? You can still see the term, but there's no need to
put it in the source file.
-- 
Robin