[TYPES] HOAS versus meta reasoning

[Karl Crary]

Well, let me just say that rather than try to peer into the mind of the 
authors of LF, I would prefer to let the mathematics stand for itself.  
I'm not aware that the theory of adequacy developed in LF was somehow 
deficient.

It's been known from the start that the power of LF stemmed from its 
apparent weakness.  In the years since LF was invented, there has been a 
lot of effort to carry out the LF methodology (now often called 
higher-order abstract syntax, or higher-order representations) in a 
stronger settting, in order to use higher-order representations and 
simultaneously do something else.  That's what I thought we were talking 
about.

    -- Karl Crary


Andrei Popescu wrote:
> I would not call the above neither concern, nor a red herring, but rather 
> state it in the form of a "naive" hope.  
> Without trying to invent pseudo-paradoxes, I would just like to point 
> that the idea 
> behind the HOAS paradigm (as I see it) was in itself something that 
> looked like a naive hope, coming from the "logical fallacy" of confusing 
> the object-level with the meta-level: 
>
> "When I consider the lambda term <<lambda x. E>> why can't I assume that 
> "lambda" is not just a representation of a function abstraction, but 
> it *is precisely function abstraction*? "
>
> Of course, this "naive" hope has received sophisticated solutions,  
> and the references of this thread witness this.  (A 
> similar situation being the "naive, non-mathematical" equations written
> by Christopher Strachey to 
> express the meaning of programs that later received mathematical 
> justifications from the domain theory of Dana Scott.)
>