On Mon, Jul 21, 2014 at 2:20 PM, Matt Oliveri <[email protected]> wrote:
> On Mon, Jul 21, 2014 at 12:18 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > The proof can be automated or manual. I > > think a better way to say your last point is that curry-style systems > don't > > work very well (subjectively) if the proofs cannot be discharged > > automatically. > > > I don't see why Church vs. Curry alone would influence how hard proofs > are to deal with. In curry-style typing, you need to be able to derive types from annotation-free programs. If the resulting discharge obligations become visible to the programmer as manual proof obligations, you're doomed.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
