[POPLmark] [Provers] Re: Adequacy for LF

[Karl Crary]

Geoff, let me make sure I understand you correctly.  You made the 
unsubstantiated claim that closure conversion cannot be done in HOAS, 
but somehow that claim has to stand until I demonstrate conclusively 
that it can?  I'm saying that you should limit yourself to things that 
you know to be true.  Sure, if you insist, you may say that problems 
that have not been attempted are open, but that sounds like a tautology 
to me.

I'm sorry about the tone, but I am growing frustrated with this.  You 
are holding HOAS to a higher level of scrutiny when, so far, it is the 
only technology that has been shown to be practical for doing this sort 
of work.  It seems as though your preference is for systems in which 
everything is possible and little is feasible, over a system in which 
many things are both possible and feasible.

    -- Karl


>> Let me make a more general comment.  Many of the criticisms levelled at
>>LF here have been of the form "you can't do X in LF/HOAS," and so far,
>>all of those have been wrong, or at least unsubstantiated.  So why don't
>>we declare a moratorium on that sort of thing.  Instead we can say that
>>some things require some ingenuity to represent in HOAS, a statement on
>>which we should all be able to agree.
>>    
>>
>
>	I'm not sure I agree.  You've said closure conversion would
>  require ingenuity, but you have not actually exhibited that it is
>  possible.  Without a solution in hand it would be more acceptable to
>  agree "that it is an open problem".
>
>  
>