Back from Reflection'99

[iepos@tunes.org]

> I also wanted to announce a completely new and revised version
> of my article "On the Notion of Implementation",
> with an illustration based on Concurrent Garbage Collection.
> I submitted it to POPL'00 <http://www.cs.wisc.edu/~reps/popl00/>
> a few minutes before the deadline, so it's too late for pre-submit
> comments (I'd like to thank my fellow PhD student Fabien Delpiano
> for the very productive help he gave during the last few days and nights).
> 
> The article is in
> 	http://www.tunes.org/~fare/tmp/implement1/

aack! ps and dvi. (:-))

> the full LaTeX sources are available at
> 	http://cvs.tunes.org/cgi-bin/cvsweb/fare/fare/reflexion/

hmm.. all I can find looks like binaries. it must be that cvsweb thing.
hmm.... could you maybe make an html version?

> I hope it's more readable than in its previous form.
> Actually, I hope it's readable enough to be accepted by the POPL committee!
> Answers on September 27. Meanwhile, comments welcome.
> 
> Hum. I have no more excuse to not begin coding. Or maybe I can instead
> write this controversial paper on the notion of universal language,
> or make lambdaND readable and split it so as to submit it somewhere...

Hmm.. I'm thinking about starting coding again also... not on a
magical theorem prover that could find TUNES using just a spec...
instead, I'm thinking of making just a more ordinary operating
system, based on instructions; it would hopefully implement many
TUNESish features like orthogonal persistence and reflection while
leaving open the possibility for full general-purpose automated
reasoning. anyway, the language(s) in the system will be applicative
(binary application as the only construct) and based on combinators
for representing sets and quantified statements, and instructions
will be ordinary constructs in the language, and there will not
be the confusion between execution of instructions and evaluation
of expressions. there will be some automated reasoning in the system
(that is, reasoning other than simple execution of detailed instructions),
perhaps resolution of definitions and maybe horn clauses; other things
i may add over time...

of course, now this is only a dream (i've coded basically nothing),
but I think it foreseeably implementable (unlike my magical
reasoning system). I'll probably start by writing a (non-reflexive)
prototype thing in C, with limited user-interface. I'll use that to
construct a sort of compiler which will generate the real image.

anyway, I'd be interested in reading your paper, Fare. If you could,
a text or html version would be real nice.

- iepos