Jon, it is you who's writing about compilers using types. I spoke of generic implementations i.e. interpreters. Sorry, I don't care about concrete representations of values. All I am interested in is that the "definitional interpreter" can tell which values are good and which ones are bad. If, later on, some proof system can improve the implementation, fine by me. Our soft typing research program has shown that we can do this for Scheme. -- Matthias