[Ur] Ur/web type system and security

[Adam Chlipala]

Anthony Di Franco wrote:
> Ok, I thought there were both a type system with some nice properties
> and at least the starting makings of or hints at an inference
> algorithm that exploits them in the OTT paper.

General type inference is undecidable in any of the languages that the 
OTT proposal is targeting.  You either apply some very domain-specific 
rules, or you get very weak inference.

> So I guess the
> question becomes, is OTT incompatible with Ur's type system, and if
> so, how?

Ur's type system is much simpler, in terms of which constructs appear.  
The magic in the Ur/Web compiler is in applying high-level "definitional 
equality rules" that would show up as explicit coercions in Coq or OTT.

> Would the heuristic approach of Ur benefit from knowing
> about the regularities OTT apparently (to me) can make evident,
> practically speaking?
>   

I see no advantages for folks programming with Ur/Web.  Most of the type 
constructors treated explicitly in the OTT paper are not present in Ur.

> Formally speaking, how sure are you about Ur's heuristics?  How does
> one falsify a wrong one?
>   

In src/coq in the distribution, you can see a formal embedding of the 
key features of Ur into Coq.  The heuristics correspond to equality 
lemmas, which can be proved sound with respect to that model.