garbage collected forths

[Hendrik Boom]

On Thu, Apr 28, 2005 at 06:50:20PM +0200, Massimo Dentico wrote:
> 
> Hendrik Boom wrote:
> 
> 
> >The ancient archives of this mailing list contains a discussion
> >"types and operators" (Thu, 13 Jun 1996 10:59:04 -0400 (EDT)),
> 
> For reference: "types and operators", Nathan Hawkins
> 
> http://lists.tunes.org/archives/tunes-lll/1996-June/thread.html
> 
> 
> >which I found using Google.  Did any of the proposals for a
> >garbage-collected Forth ever see the light of day?
> 
> Not that I'm aware of, from our part. But I suggest that you have
> a look at these nodes on our Cliki (a Wiki):
> 
> - POP-11, http://cliki.tunes.org/POP-11
>    Part of Poplog system http://cliki.tunes.org/Poplog
>    Most mature, used in British AI community. IIRC dual Virtual
>    Machine architecture, GCed, an open stack (Forth-like), an open
>    compiler (Run-Time Code Generation) and other goodies.
>    Syntax is mostly Algol-like but I think there are no problems
>    in manipulating programs (being the compiler open).

This one has potential.

> 
> - Joy, http://cliki.tunes.org/Joy
>    somewhat the "pure" concatenative language, much more
>    experimental. GCed.

Ugh Rewriting is slow.

> 
> - Factor, http://cliki.tunes.org/Factor
>    a more pratical implementation of "a Forth with GC".
>    Evolving at a fast pace. GCed.

THis one has potential, too.

> 
> - RPL and RPL/2 (Reverse Polish Lisp) http://cliki.tunes.org/RPL
>    http://cliki.tunes.org/RPL%2F2
>    originally used on HP calculators, a mix of Forth and Lisp.
>    Not sure, but probably it is *not* GCed.
> 
> and - why not?
> - Postscript, http://cliki.tunes.org/PostScript
> 
> Tell me if you are interested in type checking stack-based
> languages, I have some references to give you.

Yes, please.  I consider strong typing to be essential
for the programmer's sanity, even if no attempt is made
to use it for greater run-time eficiency.

> 
> 
> >If so, it could be an ideal platform to which to port some
> >of the work I'm doing on program transformation and verification.
> >
> >-- hendrik
> 
> Interesting. Do you have a web page about your work?
> 

No.  I should construct one.  Let me try to remember to write
you when I have.  Or remind me if I forget.

I wrote a verifier using intuitionistic type theory about
twenty years ago, on a conbination of hardware and software that's
no longer available.  I'd like to redo it now that machines are a
thousand times faster.

But in the meantime, I've noticed that the notation in which
coq (another ITT-based theorem proof-checker) archives its
proofs and theories is a stack language.  And I've got the
idea that it make sense to use Forth-like tools as intermediary
metween high-level languages and machine code.  And somehow I
think that all these ideas can come together into a coherent,
usable system -- taking my language from twenty years ago,
synthesising proofs of programs,  converting to low-level
Forthish notation,  and checking these proofs while generating
machine code.

None of these things by themselves seems too big to tackle,
except they've  gotten my mind tangled into one metarecursive
lump.

Yes, I plan to go all the way from formal theory to machine code.

-- hendrik