[Ur] Ur/web type system and security

[Anthony Di Franco]

On Mon, Sep 14, 2009 at 15:18, Adam Chlipala <adamc at impredicative.com> wrote:
> 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.

I'm asking whether Ur has somehow committed itself to only taking an
heuristic approach to dependent types, or whether some more principled
approach with enough power to be interesting (OTT) could also, or
instead, be used by it to type programs.

> Could you describe
> a concrete change to the compiler and an example program that would benefit
> from that change?

The concrete change to the compiler / language would be to make it use
OTT to type programs, instead of or in addition to the heuristics it
already uses.  I'm incapable of thinking of an example program due to
lack of familiarity with the alternatives in question, but the general
idea is there might be something your heuristics can't type but that a
really principled but still powerful approach, which is what I take
OTT to be, could.  No one may ever care in practice, of course.  I'm
just interested from a distance in how things in dependently-typed
languages are shaking out.