[Ur] Ur/web type system and security

[Anthony Di Franco]

On Sun, Sep 13, 2009 at 12:32, Adam Chlipala <adamc at impredicative.com> 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
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>