The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Adam Koprowski wrote:
>   Still I completely miss why would Program be any inferior to refine 
> for such examples, [...]

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