RE: [Axiom-developer] RE: Cast = pretend in Spad/Aldor?

[Bill Page]

But, but, ... he sputters ...

I thought Axiom was supposed to be a system for mathematicians,
or at least a system to do mathematics by computer. From that
point of view there is barely a telescope long enough to hide
the dirty details of the entrails of the computer. ;)

On November 22, 2005 5:13 PM C Y wrote:
> 
> --- Tim Daly (root) wrote:
> 
> > ultimately i think the issue comes down to this: i'm a 
> > primitivist by nature and expect programmers, like myself,
> > to know EXACTLY what the machine will execute when i use
> > high level languages like spad, lisp, or haskell.
> ...
>
> While I agree this is sometimes necessary in practice,
> isn't the whole idea of high level languages to avoid this
> necessity?

I agree completely that that is the purpose of high level
languages. In fact, I doubt that one can really successfully
program in a high level language like Spad or Haskell unless
you first accept the abstraction. Even in Lisp (which from
my point view is more like an assembler language for a high
level machine) one must accept the abstraction of the Lisp
"machine". It doesn't do you much good at all to know that
once upon a time on some machine or other (IBM 704 actually)
CAR actually "means" Contents of Address Register and CDR
actually "means" Contents of Decrement Register.

> > ... 
> > your approach to programming "from the other end of the 
> > telescope" tends to view the machine as a distant abstraction
> > and expect programming languages to properly support their
> > abstractions in all their various nuances.

The "telescope" analogy isn't too bad, but a better one might
be something like a "ladder". The machine is not viewed
as a "distant abstraction", quite the contrary, it is the
foundation on which the ladder rests. When I am at the top of
the ladder I only need to know that it is still there acting
as the foundation, but I do not care any longer what it is
made of. But yes I do expect programming languages to properly
and fully support all of the abstractions upon which they are
based. I don't have the time or energy to always climb down
the ladder each time I need another nail for the shingles. :)

> thus, you expect that
> > 
> >    type-thing :=               other-type-thing
> >    type-thing := (cast)        other-type-thing
> >    type-thing := (coerce)      other-type-thing
> >    type-thing := thing pretend other-type-thing
> > 
> > to "do the right thing"

Well, I do expect the "right thing" to at least be well
defined, even better if it serves some useful purpose. I
think this is the approach taken in almost all high level
languages.

> > and i tend to run (disassemble) to figure out what it
> > ACTUALLY does on the machine.
> 
> I thought this might be a good use for unit testing actually -
> defined the "right thing" on a per-abstraction basis and
> verify that it actually does happen on a per-machine basis?

Yes, that's ok for me. But I tend to think of it in more
abstract mathematical terms. When I define abstract data
types I think in terms of the abstract algebra that is
generated by the operators on these structures. It is how
these operators behaviour - the rules that they should obey
that defines this object from an external point of view.
The job of unit testing is to verify that the representation
of this abstract algebra in terms of operations at the
machine level is "faithful". The concept of a faithful
representation is one that is used frequently in mathematics,
e.g. in group theory.

In principle, disassembly is one of the steps in the proof
that a representation is faithful. But that can only be done
if we first have a rigorous definition of the abstraction
itself.

> 
> > Axiom DOES support strong static typing but (at least in my
> > view) it isn't a closed semantics language so sometimes you
> > have to know the internals. in your view the primitive
> > domains would export operations that hide the implementation,
> > fully support the abstractions and have closed semantics.
> 
> At least at the Spad/Aldor level, isn't this desirable?  Or
> would BNatural be the logical level for "bullet-proofing" in
> this fashion?

I think you were right on the first answer. From my point of
view it is absolutely essential at the Spad/Aldor level if we
are in any correct sense to think of these a programming languages
in and of themselves, independent of a specific implementation.

I think the issue at the level of BNatural is rather different.
BNatural is built on top of the Spad/Aldor level and the Axiom
library. It's purpose is to bridge the gap between our intuitive,
ambiguous natural language based expression of mathematical ideas
and their rigorous definition in the Axiom library. But even
here there is a need for the domains that underlie the single
ExpressionTree domain of BNatural to hide their implementation
details from the higher level.

>  
> > ultimately you want to appeal to the documentation to see
> > what a language construct means. i kneel before the altar
> > of the machine and see what it does.
> 
> I always thought what made the most sense was to clearly define
> the behaviours an abstraction needs to function properly as part
> of the documentation, and have a way in the program to test that
> those assumptions actually ARE valid.  That gives you not just
> assumption of valid abstractions but verified valid abstractions,
> and allows one to work at the abstracted level with confidence.
>

Again I completely agree with you. The documentation *must* come
first. In fact since this is mathematics that we are talking about,
the documentation almost always consists of a well developed body
of knowledge and a set of formal theorems. We want to know first
of all whether what we wrote in Spad/Aldor properly represents
this mathematical knowledge - or at least clearly delineate the
range over which this representation is accurate. Doing this does
not involving knowing exactly what the machine does at a low
level.
 
> I suspect I'm missing something though - typing related issues
> are way beyond me :-/.

As far as I am concerned you have a good grasp of at least the
basic ideas. :)

> 
> > ps. i liked programming in high school. the wang mini with the
> > hand-punched "toaster" card reader kicked ass. :-)
> 
> Heh - I always like the idea of punch cards.  They seem a lot
> more durable than any of our electronic storage methods, even
> if their data density per kilogram is a tad low.
> 

You wouldn't say that if you had to load the "dog eared" stack
of the Fortran II compiler (consisting of something like a 1000
punch cards) in front of your painfully punched and re-punched
first 10 line Fortran program for what seems like the 100th time
(not counting the 6 dozen or so miss-feeds) before getting the
reward of 50 newly machine punched cards which you then had to
append along with your single data input card to the back of the
stack of the Loader program (consisting of another 500 or so dog
eared cards), just to get the damned IBM 1401 to compute the
square root of a number ... all at about 4:00 AM in the morning,
because during the day the machine was actually used for more
serious computing.

Believe me, it was a big advance when I got to University and
we actually could do all this during the day using paper tape. ;)

Regards,
Bill Page.