RE: A mathematical foundation of reflexion?

I just wanted to add that
http://www.latrobe.edu.au/www/philosophy/phimvt/j00syn.html introduces not
only a facinating computer language, but uses that language as a notation
for explaining many computer science and mathematics problems in a very
understandable way (including basic category theory).

The language itself is essentially Forth with garbage collection, typed
data, and function quotation.  I'm impressed with the language, but I'm even
more impressed with how much easier it is to work out proofs than it is with
lambda calculus, and I'm still more impressed with how well the author has
researched and explained the implications of his language.

-Billy