OT: GCed Forth-like language, proof checking and machine code generation (was: migrating to mediawiki)

[Massimo Dentico]

Brian Rice wrote:

> But does your software really matter when there
> is Factor?
>
> http://factor.sourceforge.net/
>
> Why not just merge with Factor and take the saved
> development time to do more interesting things?


Brian,

I know you don't read the TUNES-LLL mailing list anymore,
so you don't have the proper context.

Check this thread:

http://lists.tunes.org/archives/tunes-lll/2005-April/thread.html

He has particular needs and goals; as you can read in
that thread, I pointed out Factor (but not only) to him,
so he has consciously choosed to not use Factor.

For your convenience, I quote the relevant details here:

taken from the bottom of this message
http://lists.tunes.org/archives/tunes-lll/2005-April/000169.html

> 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

[see http://cliki.tunes.org/Coq]

> 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.


Brian Rice wrote:

> Most TUNES members really do not follow what is
> actually going on in the wide world of computer
> science. That's worthless for this project, since
> the point is to provide a common convergence goal.
> The lone-wolf TUNES implementor is a FOOL.
>
> --
> Brian

Other context on the web site of his company:

http://www.pooq.com/

(it seems not reachable from here at the moment).

He is not exactly a "CS novice" (euphemism).


Regards.

--
Massimo dentico