[PRL] Type question...

[Dave Herman]

> OTOH, the Erlang community seems to be moving in the other direction.  
> They have a notion of "success typing" that says roughly, if the 
> computation succeeds, then some property holds.  As near as I can tell, 
> this seems to confuse typing with flow analysis. (Somebody here should 
> probably write a oaper sorting all this out.)

IOW, existential properties (exists a trace T . P(T)) versus universal 
properties (forall traces T . P(T))? This to me has always felt like the 
difference between the kind of reasoning you do in testing (can I 
demonstrate the existence of a successful trace) as opposed to 
verification (can I verify that all traces are successful).

Dave