search

hazelgrove / hazelnut-popl17

Submission to POPL 2017
2 stars 1 forks source link

what is the principle? #49

Closed ivoysey closed 7 years ago

ivoysey commented 7 years ago 
"This paper develops a principled solution."  What is the principle?  It
would be great to know up front succinctly the guiding principle, even more
than the names of the formalisms to be developed.
ivoysey commented 7 years ago 
"which, by its correspondence with contextual modal logic, lays logical
foundations beneath our work."  I'm not clear on whether this is a happy
syntactic accident or whether there is a compelling connection here that
should guide the development of structure editors or has more to add.  The
related work didn't really help me with this, especially since "making the
modal context explicit in our semantics is not technically useful given our
stated purpose."  So what is useful about this?

probably a related complaint. maybe we're just talking like CMU people or something? and maybe that's ok.

cyrus- commented 7 years ago

I think "what is the principle" is not a meaningful question so I'm just going to leave that part of the intro as-is unless someone objects. our solution is a "principled solution" because we actually fully characterize it per the principles of type theory.

ivoysey commented 7 years ago

i guess my only thought was that, in the little CMU bubble, i take it as read to mean that "a principled solution" is what you say -- something fully characterized per the principles of TT. i don't know if that's a generally used meaning of the catch phrase. if it isn't, people might misunderstand us or think that it's filler text, but i believe we mean something quite specific.