[Aldor-l] [Axiom-developer] spad: language and compiler

[Jacques Carette]

Page, Bill wrote:
>> Every 6 months or so, I tell Stephen he should write up a 
>> formalization of Aldor's type system, and prove the usual
>> Progress and Preservation theorems for it. 
>>     
>
> When it comes to the application of Aldor as the Axiom library
> compiler, I am afraid that demanding that Aldor satisfy these
> usual requirements might amount to "throwing the baby out with
> the bath water".
>
> The concept of "Progress" is very similar to well-foundedness.
> By direct analogy with the theory of non-well-founded sets we
> can have non-well-founded types which violate Progress but still
> satisfy Preservation.
>   
Aldor 'works'.  So if it were necessary to introduce new notions (or 
leverage recent work) to formally prove this, that would be icing on the 
cake!

As far as co-induction goes, I'm a fan too! ;-) 
[http://lists.seas.upenn.edu/pipermail/types-list/2004/000177.html]

Jacques