first: I had not previously read hehner's "beautifying godel" paper, but now that you mention it I must say that I disagree with you that it is the "work of an incompetent". I believe the paper illustrates the concept, and does so in a way which is reasonably terse and accessible to a computer programmer, and pleasantly free of the advanced latex, infinite sequent trees, ambiguous notations and ridiculous term encoding which plagued the "logicians presentation" I received in stephen cook's class. I seem to recall him even saying as much during lecture: that a interpretation-oriented presentation, over ascii strings, would probably be much easier to follow. what makes you think of it as incompetence?

second: I certainly do not like working in TCL, since it is so unsafe and more than a little awkward at times; all I'm arguing here is that string manipulation is effectively as powerful as sexp-splicing. I don't see any refutation of this in bawden's paper, merely a preference for the simplicity and "synergy" of the lisp combination. by all means, use a lisp. it's a good system, definitely. personally I prefer something even tighter: camlp4 statically typechecks my metaprograms too. are there any free lisps which do this? I haven't found them. seriously, I'd like such a thing, I just don't have one.

third: yes, camlp4 is a little "fixated" on "source vs. object code"; more accurately you could say that it's "fixated" on pre-run-time static verifications, since you can certainly ship source-only ocaml programs that compile at load-time. lisp's approach doesn't confuse me, it just isn't terribly safe. I happen to like static verifications, and am happy to trade runtime metaprogramming, a feature I do not often want, and freqently want to prohibit, for statically checked compile-time metaprogramming. if you could point me to a good, free, portable lisp with a native code compiler which does typechecking of its metaprograms and their results, and permits custom lexers for the metaprogram input, I'd be happy to investigate it. imho that is ocaml.