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

[Brian Rice]

On Oct 19, 2005, at 8:47 PM, Massimo Dentico wrote:

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

Well, ok, it's superficially interesting, and probably worthwhile,  
but not from the TUNES perspective. That is, we don't care if that's  
"why he can't help" because that's not something we're doing. It  
definitely smacks of the usual self-promotion on this list: someone  
brings up their project to us thinking that they'll gain volunteers  
or our "blessing" or something. In fact, that seems to be the only  
thing that most people consider this list worthwhile for.

> 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.
>
> He is not exactly a "CS novice" (euphemism).

I agree, but that is immaterial to my point:

We, as TUNES project members, should not endorse or pay any mind to  
projects which attempt to become new "metarecursive lumps" except via  
providing a migration path for existing software via multiple paths -  
we need software that ties things together, not a new pile of  
research legacy code. Forth dialects definitely LOSE on this front.

I see more interesting stuff pass by on Lambda the Ultimate in a week...

--
-Brian