The Coq mailing list

[Luke Palmer <lrpalmer AT gmail.com>]

On Sun, Feb 22, 2009 at 11:21 AM, Adam Chlipala <adamc AT hcoop.net> wrote:

Robin Green wrote:

 [With Program] 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.
 

Terms with coercions are _much_ harder to reason about than terms without.

I don't know why you think that you don't need the coercions if you write it by hand.

This argument seems to be more about style than just whether to use Program or refine.  The Program style is to include information about the parameters/results as sigma types, whereas I guess the refine style is not to, proving those facts externally based on the uninformative implementation given?

Luke