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. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
