[POPLmark] Adequacy for LF

[Carsten Schuermann]

> This again brings us back to the fundamental point that it is  
> entirely spurious and counterproductive to insist on some a priori  
> formulation of a language if your goal is to mechanize its  
> metatheory.  You have to listen to the logical framework, as it  
> were, and take its advice in guiding you towards a better way to  
> formulate your system.  We learned this lesson many years ago when  
> we first invented LF --- the exercise of formalizing a logic in LF  
> does wonders for the logic.

I couldn't agree more.  Countless times did LF help me improve  
language and logic designs.  It is a mistake to stay too attached to  
at a particular formulation.   Let LF be your guide. Thanks for the  
comment Bob.

-- Carsten