Re: [Axiom-developer] Re: SPAD and Aldor again

[C Y]

--- Gabriel Dos Reis <address@hidden> wrote:

> C Y <address@hidden> writes:

> OK, thanks for the explanation.
> 
> Since I'm not in the business of cloning Aldor, I'm not sure how that
> affects Axiom.

The discussions I am seeing so far seem to largely indicate that we
need to take SPAD in the direction Aldor went, at least to start with. 
This is not surprising as Aldor itself was intended to fix problems
with SPAD, as I understand the history.

> I don't see a point of cloning Aldor.  
> I see great benefits in an improved SPAD.

Certainly.  But an improved SPAD probably can't help but look something
like Aldor, since Aldor was in some sense an attempt to do a better
SPAD.
 
> | > You don't need a language to do *just* mathematics in Axiom.  You
> also
> | > need a language to communicate with the world around.  All major
> | > systems for computation mathematics have grown into that
> position.
> | > Don't get blindsighted.
> | 
> | I would prefer to let the Lisp level handle the outside world as
> | much as possible.
> 
> But you still need to specify what that does to a SPAD program.  Just
> delegating to Lisp does not solve the fundamental problem.

I guess it depends on the details of how such things are handled.  You
are proposing to have code at the SPAD level talk directly to things
like external libraries?  I guess my thought on that was to use
CFFI/other lisp tools to talk to the external libraries, and then use
the lisp level to present an API to them to SPAD.  Admittedly that's
rather vague, but hopefully we would only have to solve the SPAD<->Lisp
part of the equation and leave all the other messy details out of it.

> |  What are you referring to by communication?  Exporting
> | algorithms as Fortran code?  Interacting with C libraries?  File
> | and Data Input/Output APIs?
> 
> All of that, including interfacing with nay reasonable language used
> in the computational science community -- that list goes beyond
> Fortran and C.

Indeed.  C++, Java, Python, Haskell, CAML, ML, various proof
languages... more I'm sure that aren't leaping to mind.  You know more
about those things than I do Gaby, so perhaps the difficulties are less
severe than I am imagining, but I was under the impression that
translating from one language to another is highly non-trivial. 
Particularly if the program is written in such a way as to assume
communication only with other Java/C/ML/etc. programs.  Lisp's FFI
systems are probably among the most general solutions to such problems,
and even they have a host of issues.  And if we want to eventually
support formal verification and proof generation multiple languages
could exponentially complicate the question - in such circumstances we
would have to query libraries not just for functionality but for proof
that said functionality is correct - and how do we verify the proof
matches the implementation in an external library we may not even have
source code for?  md5 sums some kind?

I wish I knew more about such things.  I suppose at some level any
Turing complete language can express ideas expressed in other
languages, so perhaps there are techniques I'm not aware of.

Cheers,
CY


 
____________________________________________________________________________________
Sponsored Link

Online degrees - find the right program to advance your career.
Www.nextag.com


 
____________________________________________________________________________________
Sponsored Link

Mortgage rates near 39yr lows. 
$310k for $999/mo. Calculate new payment! 
www.LowerMyBills.com/lre