[Ur] Ur/web type system and security

[Adam Chlipala]

Anthony Di Franco wrote:
> 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'm having trouble understanding what you're proposing.  Could you 
describe a concrete change to the compiler and an example program that 
would benefit from that change?