[Ur] Ur/web type system and security

[Adam Chlipala]

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.