A plan for implementing TUNES

[Guillaume FORTAINE]

Hello,

I believe that there are great thougths in this mail.However, I will try to 
enhance it, because there are some major mistakes.

Michael FIG wrote  Thu Aug 3 08:35:36 PDT 2006

>Hi,

>I am a professional project manager and cybernetician. I have been
>studying TUNES (http://www.tunes.org/) for several years, and have
>come up with a project plan to accomplish it. I am running it past
>you to see what you think, but honestly, I will work on it whether you
>want to cooperate or not, as is my freedom with free software.
>However, I would be happier if you joined me. :)

>My home page (in my signature) fully explains my history and
>intentions, which you can explore at your leisure.

>I propose a layered architecture:

>6. Category Theory
>5. Specification Language
>4. Dynamic Compiler
>3. Runtime Environment
>2. Computational Model
>1. Virtual Machine
>0. Hardware

>Here are the URLs of the best-of-breed free software I have chosen to
>fulfill these requirements.


>6. Arrow - http://tunes.org/~water/arrow/

Please see : http://www.haskell.org/arrows/

Arrows are a new abstract view of computation, defined by John Hughes [Hug00]. 
They serve much the same purpose as monads -- providing a common structure 
for libraries -- but are more general. In particular they allow notions of 
computation that may be partially static (independent of the input) or may 
take multiple inputs. If your application works fine with monads, you might 
as well stick with them. But if you're using a structure that's very like a 
monad, but isn't one, maybe it's an arrow.

>5. Epigram - http://e-pig.org/

Please see  : 

http://www.dcs.st-and.ac.uk/~eb/esc.php

ESC, the Epigram Supercombinator Compiler, is a simple functional language 
which compiles to efficient (well, maybe!) C code. The primary aim is to 
develop a back end for Epigram, but it will (I hope, eventually) be useful to 
anyone looking for a back end for a functional language.

http://repetae.net/john/computer/jhc/

jhc
jhc is a haskell compiler which aims to produce the most efficient programs 
possible via whole program analysis and other optimizations


>4. Pliant - http://fullpliant.org/
>3. Figure - http://fig.org/figure/figure.txt (also see The Circle of
>   the Promises http://fig.org/figure/CircleOfPromises.pdf.)
>2. An amalgamation of the Mozart (http://www.mozart-oz.org/), E
  > (http://erights.org/), and Erlang (http://erlang.org/) models
>1. Factor - http://factorcode.org/

You don't need 6 languages ! 1 will be enough :

http://programatica.cs.pdx.edu/House/

Haskell User's Operating System and Environment, version 0.8, August 2006
House is a demo of software written in Haskell, running in a standalone 
environment. It is a system than can serve as a platform for exploring 
various ideas relating to low-level and system-level programming in a 
high-level functional language. More details are available in our ICFP 2005 
paper: A Principled Approach to Operating System Construction in Haskell. 

>0. Optical computers - http://en.wikipedia.org/wiki/Optical_computer

I believe that FPGAs will be better :

http://en.wikipedia.org/wiki/FPGA

http://srg.cs.uiuc.edu/twiki/bin/view/OpenFPGA/

http://www.openfpga.org/


>None of these systems is yet complete:

There are almost complete and FPGAs are available ;) !



I look forward to your answer,

Best Regards,

                     Guillaume




PS : I believe that we are near a fomally verified AI :

-Separation Logic :

http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html

http://www.bcs-facs.org/events/EveningSeminars/slides/richard_bornat_08_12_05-handouts.pdf

http://en.wikipedia.org/wiki/Separation_logic

 
Separation Logic a term attributed to John C. Reynolds, is an extension of 
Hoare logic that describes variations on program logic in computer science.
In particular, separation logic facilitates reasoning about:
programs that manipulate pointer data structures — including information 
hiding in the presence of pointers;
"transfer of ownership" (avoidance of semantic frame axioms); and
virtual separation (modular reasoning) between concurrent modules




-Deep Inference and the Calculus of Structures  :

http://alessio.guglielmi.name/res/cos/LD/index.html

http://wwwhomes.doc.ic.ac.uk/~ozank/Papers/aia05.pdf

Towards Planning as Concurrency
 Ozan Kahramanogullari

We present a purely logical framework to planning where we bring the 
sequential and parallel composition in the plans to the same level, as in 
process algebras. The problem of expressing causality, which is very 
challenging for common logics and traditional deductive systems, is solved by 
resorting to a recently developed extension of multiplicative exponential 
linear logic with a self-dual, noncommutative operator. We present an 
encoding of the conjunctive planning problems in this logic, and provide a 
constructive soundness and completeness result. We argue that this work is 
the first, but crucial, step of a uniform deductive formalism that connects 
planning and concurrency inside a common language, and allow to transfer 
methods from concurrency to planning.