On Sun, Sep 13, 2009 at 12:32, Adam Chlipala <[email protected]> wrote: > Anthony Di Franco wrote: >> >> - I just glanced at the paper "observational equality, now!" and it seemed >> pretty appealing although I lack the background to grasp the finer points. >> What is the relationship of the ur/web type system to one along the lines >> therein, relative tradeoffs between them, could the ideas there be >> implemented for ur/web, are they in some maybe partial sense already? >> > > One of the main motivations for OTT (the system from that paper) is to make > it easier to reason about programs that manipulate proofs. There are no > non-trivial "proof objects" in Ur/Web, so it's not clear that the details of > a formal definitional equality are so important. The definitional equality > in Ur/Web is already fairly fancy, including some algebraic laws about > 'map'; it's nowhere near as principled as the definitional equality of Coq > or OTT, since I add new typing heuristics as they seem useful. :)
So, could OTT be used among Ur's set of heuristics as a way to type programs that works alongside your other heuristics? If not really, what would need to change? >> - I glanced at the demos and saw that to be really functional state is >> often passed in the url. What techniques are used to avoid the security >> pitfalls of dangling application state out like that while remaining >> idiomatic? >> > > There are no such security measures included automatically. When writing a > Ur/Web application, you must assume that all in-scope variables can be > "havoced" across any call from client to server. > > _______________________________________________ > Ur mailing list > [email protected] > http://www.impredicative.com/cgi-bin/mailman/listinfo/ur > _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
