Reasoning about TemplateMonad commands?

[jsarracino]

Hello,

This is more of a question than a real issue, but I wasn't sure how best to reach folks, so I'm putting it here. I've been using MetaCoq and TemplateMonad for developing a plugin (it's really usable and slick, great job!) and it would be great to reason about the result of running TemplateMonad programs (even axiomatically).

Is there currently a way to do this, or plans (even tentative) to implement something like it? For example, it would be nice to reason about the effect of tmMkDefinition on the global environment, or the behavior of tmLocate, etc.

Thanks,
John

[TheoWinterhalter]

The best way to reach us is probably on the Metacoq zulip stream of the Coq zulip: https://coq.zulipchat.com/

For now we have no specifications for these operations. I guess it could be interesting but I'm not sure anyone is working on it.