Stream: MetaCoq

Topic: Template and PCUIC

view this post on Zulip Meven Lennon-Bertrand (Feb 13 2023 at 11:28):

Jason Gross said:

But I guess PCUIC will probably be easier to build typing derivations for, if I want to eventually use the safechecker?

It is somewhat weird to me (and I think I heard @Théo Winterhalter express this view as well), that the safe-checker is not written for Template (which is supposed to be the closest of the two systems to the actual implementation), but for PCUIC (which is mostly designed to make for an easier meta-theory).

Indeed, I can see a world where the two start to diverge more. For instance, as some point we talked about forcing constructors to be fully applied in PCUIC. It might also be the case that to have a meta-theory go through for typed conversion we have to add annotations that are redundant from the point of view of implementations, which we probably don't want to add to Template even if we are forced to add them to PCUIC. If this happens, having the safechecker for PCUIC would become more and more weird…

I don't know what the other MetaCoqer think of this, but maybe we should at some point consider the possibility/cost of switching the system on which the safechecker operates?

view this post on Zulip Théo Winterhalter (Feb 13 2023 at 11:36):

Yes, I also think it does not make sense to verify a checker in PCUIC, it should be in Template so we can clearly separate the efficient, implementation-driven TemplateCoq and the meta-theory-ready PCUIC.

view this post on Zulip Matthieu Sozeau (Feb 13 2023 at 12:37):

I agree but it was not a simple thing to do a few years back. Now with all the metatheory in PCUIC and the Template-PCUIC translations it might be feasible to use it to do all the heavy reasoning while working on the template implementation.

view this post on Zulip Meven Lennon-Bertrand (Feb 13 2023 at 13:59):

I see, this makes sense :) Let's keep this somewhere in mind if/when someone has the courage to pick up the challenge! As I was saying, this might pop up if we investigate typed conversion, so maybe we'll have to bite the bullet at some point there

Last updated: Oct 13 2024 at 01:02 UTC