24 Sep 2002 graydon   » (Master)


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.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!