advotake: A nice quick hack; use expect as an intelligent xml-rpc client to post advogato diary entries.
redi's proposed hack: <quote>redi </quote> I like the idea. I think `redirect' is a better name, though...
graydon: I think the thing I have enjoyed most in our past communications is discovering just how differently it is possible for an intelligent and well-informed computer scientist to view the field of programming languages. From some of your past posts, in no particular order:
- TCL: Actually Tcl is one of my favourite languages (in the guise of Don Libe's `expect'). I just don't think that string manipulation is `real' syntactic metaprogramming. To my taste, Alan Bawden's `Quasiquotation in LISP' article presents the definitive case against string manipulation as meta programming.
- Hehner's introduction to Goedel's proof at his website is the work of an incompetent. Maybe he just had a bad day...
- I've had a look at camlp4 (at last): it's a nice solution to a problem that doesn't arise in languages like LISP that don't get fixated on `source code' vs `object code'. Because in LISP-like languages (read <file>), (macro-expand <s-exp>) and (eval <s-exp> <environment>) are just normal programs, the semantics of the language need make no distinction between read time vs run time, or between interpreted code and compiled code. It confuses beginners, but once you've grokked the basic idea it makes life much simpler.
raph: I very much like the way your ideas are going with web-based proof assistants. Some thoughts:
- On proofs amd code - I recommend reading Euclid's Elements; there are a lot of parallels between what you say and the way he goes about constructing his arithmetic and geometry;
- I think tactics were invented by LF-ers, not HOL-ers. I suppose HOL is based on the Edinburgh LF (the chaps who invented ML in the 1970s);
- I think the `right' logic for most purposes (ie. the axiomatic framework we might the `east pole' on the `more mathematical' scale of Wiedijk's graph) is classical second-order arithmetic. It is probably the most intensively studied strong proof theory in mathematics: it pretty much immediately encodes all weaker systems, and most stronger systems can naturally be expressed in it.
Bram: You can protect against this kind of thing (buffer overflows, character set attacks, etc.) on either the server or client side by applying the `command' design pattern and then embedding the control language in your favourite tcl-alike.
http://www.advogato.org/person/Roger/: Is there a clean correspondence between SlideML and Slatex?
suse->debian: I've converted my laptop from a Suse 6.4 box to a stable debian woody. Pretty smooth, but a few lumps are proving difficult to iron out:
- My X server crashes when I suspend. An ugly apmd vs. XFree86 vs. Trident vs. God knows what else conflict.
- I can't get video output and laptop display from the same client plane.
- Debconf has put an ugly network environment script in my init.d directory which I can't track down.
- I have a funny DNS vs. wwwoffle conflict.
- The usual round of trouble with .Xresources being handled differently by every other program...
reading: Wittgenstein's Lectures on the Foundations of Mathematics. I'm a glutton for punishment...
work: is going well |-D