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. :)
- 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
