On Thu, Jul 10, 2014 at 6:22 PM, Geoffrey Irving <[email protected]> wrote:
> If we manage to go the extensible proof checker
> route, we can make everyone happy (or at least as happy as can be
> expected).  Let's move this discussion to the thread I just started
> with the better name.

I don't think extensible checking helps here. If I'm understanding
correctly, Shap will not want to use language features unless someone
comes up with sufficiently well-behaved type inference for it. In
principle, extensible checking would allow the inference to be added
outside the core language, but if there _is_ no way to do inference,
some features shouldn't have gone into the core language in the first
place.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to