A plan for implementing TUNES
guillaume.fortaine at wanadoo.fr
Sun Jan 14 11:25:06 PST 2007
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
>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
>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 :
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.
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 :
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 :
>None of these systems is yet complete:
There are almost complete and FPGAs are available ;) !
I look forward to your answer,
PS : I believe that we are near a fomally verified AI :
-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 :
Towards Planning as Concurrency
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.
More information about the TUNES