A mathematical foundation of reflexion?

[btanksley@hifn.com]

> From: Laurent Martelli [mailto:martelli@iie.cnam.fr]
> Subject: Re: A mathematical foundation of reflexion?

> >>>>> "John" == John Carter <cyent@mweb.co.za> writes:

>   John> I think Joy lays bare that special something about Forth and
>   John> Postscript.  The homomorphism between syntatic concatenation
>   John> and functional composition. If that homomorphism exists, then
>   John> reasoning about the program becomes very much easier, and if
>   John> reasoning becomes easier it is much easier to write bug free
>   John> programs.

> I'm not so sure. I think that the absence of named parameters can make
> it difficult to understand programs. 

An excellent question.  In my experience, this can easily be a problem when
the programs deal with too much input at a time; however, very few problems
can't be broken down, and in Joy (if not in Forth) the multiple parameters
of the problem can easily be condensed into a single object.  (Although Joy
would still do well to provide more facilities in this regard, since
currently the only type of truly generic object organization which Joy
supports is a list.)

In other respects, Forth has already demonstrated that even if you don't
know the language implicit parameter passing can make it easier to read (in
an abstract sense); the reader doesn't have to know about parameters, only
about actions being taken.  Debugging requires more knowledge, but debugging
is also simplified by the implicit parameter passing because any
syntactically complete portion of the program can be lifted out and tested
in isolation (the language is not only truly referentially transparent, it's
also almost fully context-independant).

Finally, the Joy papers demonstrate how easy it is to prove certain basic
facts using the notation of the language itself.  It's FAR simpler and
clearer than the same proof is in lambda notation or even in any invented
notation I've seen, and if the proof is clearer in the language, programs
written in the language have a MUCH higher chance of being both obviously
and provably correct at the same time.

> Laurent Martelli

-Billy