Re: [Axiom-developer] Aldor and Lisp

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> writes:

| On Tuesday, October 18, 2005 6:43 PM Gaby wrote:
| > 
| > "Page, Bill" <address@hidden> writes:
| > 
| > | ... Aldor is a complex very high level language - not so
| > | different from Haskell or Ocaml and it certainly took a major
| > | effort to implement usable compilers for those languages.
| > 
| > Indeed.  But the positive side of it is that those are now part
| > of common knowledge and it is not like everything has to be
| > rediscovered over again.  We have more foresight -- based on
| > the accumulated knowledge -- than they did when they started
| > implementing those compilers :-) And I bet the experience with
| > Haskell or Ocaml or functional language with dependent types
| > will be valuable for implementing Aldor.  So, while I agree
| > with your points, we must also keep in fore that one would not
| > start totally "clueless"...
| > 
| 
| I agree. In fact to take best advantage of this knowledge, perhaps
| we might seriously consider the possibility of writing "new Aldor"
| in a language like Ocaml. I think Ocaml might be a better choice
| than Haskell since both Ocaml and Aldor are not strictly functional
| languages like Haskell. 

Haskell is not strictly functional either -- despite the banners.
It has an imperative skin.

That said, I would not like to get into "language war".  My compiler
implementation experience is with languages like C, C++ and Haskell --
for writing compilers for those language in themselves.  

| Also, given the interest in applying proof techniques in Axiom,

My current work on designing and implementing a general, efficient,
scalable, complete representation of ISO C++ (with concepts) in C++
has led me to look at the materials on proof techniques in Axiom.
I've read claims that Type:Type is inconsistent with
types-as-propositions stance.  I'm curious to learn how the type/proof
techniques in Aldor would get away with that. 

-- Gaby