RE: [Axiom-developer] Questions

[C Y]

--- "Page, Bill" <address@hidden> wrote:

> On Thursday, September 15, 2005 3:27 PM C Y wrote:
> > 
> > I suppose I should know better, but I have a couple "broad
> > scope" questions about Axiom:
> 
> I really like your questions! I would like to see more
> discussions of this kind.

Heh - thanks :-).  I remember my uncle saying once that the only way he
rebuilt a country farmhouse into a really nice family home was by not
knowing how much work it was going to be - I sort of wonder if that's
me looking Axiom over ;-).

> > a)  Given the ideal of theoretically backing the mathematics
> > in Axiom and perhaps even incorporating a proof system into
> > the core design, how do we handle/document/formalize the
> > interface between "Axiom-level" code and the underlying lisp
> > functionality?  Ideally, a "provable" system would be backed
> > by proofs all the way down to the machine code and chip design
> > levels, but that's well beyond the scope of the Axiom project.
> 
> Agreed.

Hopefully the Coyotos project will get somewhere, but they're still
busy designing a language that will work for what they want to do,
IIRC.  Oh, well - maybe in 30 years ;-).

> > I'm assuming the point we would want to start using proof
> > logic is the point where the actual "mathematics" beings, as 
> > opposed to the computational tools and structures needed to
> > support it - is this correct?
> 
> Yes I think so. To me this means specifically the SPAD and/or
> Aldor code from the Axiom algebra library.

Right.  Although I think it is important to try to understand
thoroughly how the basic tools used at the SPAD/Aldor level interact
with their "computer level" support structure.

> > Effectively treat the behavior of the underlying lisp as a
> > big set of "axioms" (in the mathematical sense) and build
> > off of them?
> 
> From my point of view lisp has very little to do with this
> issue. Sorry. :) 

No problem - I had assumed lisp was critical to Axiom.  Either way,
assume the "computer" behavior is as specified.

> Consider the fact that the Aldor compiler can
> output C code which then gets compiled into machine code by a
> C compiler like gcc, just as easily as it can produce lisp code
> that either gets interpreted or compiled in turn. To say this
> with a positive spin: Lisp is too general and flexible a language
> to be well suited to mathematical proofs.

Well, I'm not going to argue that lisp isn't extremely general ;-). 
It's a good point.

> A "higher level", i.e.
> more semantically constrained and focused language (in the sense
> of having a smaller set of more complex primitive operations)
> such as SPAD or Aldor, is better suited to expressing mathematical
> algorithms nearer the conceptual level at which mathematics
> itself is done. Of course this is not a claim that such is not
> possible in lisp - it's just that the language (or maybe
> sometimes just common practice) does not encourage such usage.

Right.  I think for this we want to stay as close to the math as
possible, so I'll agree with you there.

> The point is that the "meaning" or semantics of SPAD and Aldor
> programs can be specified quite independently of the actually
> implementation. Most of this specification of meaning actually
> involves known mathematics to a much larger extent then the
> usual application of proof techniques to the correctness of
> programs in general. I think a claim could be made that
> proving that a particular algorithm written in SPAD correctly
> implements some specific mathematical result or technique might
> be considered formally less difficult (in principle) than
> general program correctness because most of the proof can be
> carried out at a higher level.

Not sure about that one.  Sounds reasonable though.

> I think you are right that proving the correctness of the
> compiler itself or the interpreter needs to be addressed at
> a different level. Even within Axiom there are several
> intermediate levels, e.g. BOOT code, that could be addressed
> separately. Then all the way down to machine code and from
> there (in principle) even to the physics. But for *mathematics*
> I think (almost) all of the interesting stuff is at the
> top of this hierarchy of languages.

OK.  I think the intermediate levels should at least be thoroughly
documented though, so if someday it becomes possible to really apply
proof techniques to them too it's easier going for whoever tries it. 
Plus, we can probably find bugs more easily that way ;-).
 
> > b)  If we are interested in using Aldor as opposed to Spad for
> > the "standard" Axiom language, and are forced to re-implement
> > an Aldor environment due to licensing concerns, would that be
> > the time to build in proof systems and tools?
> 
> Personally I think that failure to include Aldor in with Axiom
> because of licensing issues would be a minor disaster for both
> Axiom and Aldor.

I don't disagree, but the Macsyma Inc. experience is sufficient warning
that depending on non-open and/or non-free code is not viable if one
wants to be sure of long term viability and potentially universal
usage.  That's the reason license issues always generate so much
discussion - people know how important they are in the long term.  I
think we should act fairly soon to clarify the Aldor situation, but I
don't know where the situation stands any more.  This
(http://aldor.org/license-rationale.html) was written some years ago,
and I don't see much recent activity on the Aldor list except from
Axiom folk.

> I doubt very much that sufficient interested
> resources exist anywhere at this point to take on a task like
> re-implementing Aldor. Implementing a compiler for a language like
> Aldor is already a very BIG job. And imagining adding a program
> proof systems on top of that at the same time does not makes much
> sense. 

Well, I was thinking the proof subsystem would need to be integrated
into the Aldor language itself, but perhaps not.  Anyway, I would be
very definitely against Axiom becoming dependant on non-free software,
whatever the potential gains might be.  

> Also keep in mind that there are a number of very active
> projects in this area already such as Haskell, OCaml and OBJ
> (to name just a few).

Would those be relevant to Axiom?

> > Or even if we don't have to redo the environment - mightn't it
> > still be the time?  Then as we convert things over to Aldor,
> > document them and prove relevant properties?
> 
> Yes, I think that is the right approach! That is exactly where
> Tim's ideas about literate program should be the most use.

:-).  That should be very interesting!

> > c)  I know it's somewhat impractical, but I like the idea of
> > implementing something once, correctly, documenting it fully,
> > and then never having to do it again.
> 
> I don't think that is just impractical I think it has been
> demonstrated many times over that it is *impossible*!

Well, I suppose it depends on how you look at it.  

> From my
> point of view good programming practice these days amounts to
> finding ways to do many of the same things over again, in fact
> several times over, but to do it efficiently and with (much)
> less pain. We need methods for fluently "re-factoring" programs
> at a very high level - iteratively re-thinking, documenting and
> re-implementing the basic internal design and the relationships
> between the components.

I was hoping being close to the mathematics would help keep things
organized in that regard - not to say a new, more efficient
proof/algorithm couldn't supercede an old one, but ideally the rest of
Axiom wouldn't have to worry HOW a particular piece was proven or a
particular algorithm was used.

> This is one of the essential tasks of
> high level programming language design. I think one of the
> fascinating aspects of programming languages like SPAD and Aldor
> is that they do in fact seem to facilitate this process.

I must confess I don't quite follow here.  Let's say we implement the
Risch algorithm for integration, and subject it to the relevant proofs.
 Won't we be able to work off of that implementation and not have to
create it again elsewhere?

> > Axiom gets closer to that ideal than virtually any other system
> > I have seen (well, except maybe TeX ;-)
> 
> (: choke, cough :)

Heh.  Of course, it could be that nobody dares to touch it, either...
;-)

> I think it is much easier to prove "conditional truths",
> i.e. proving that the output of a particular algorithm written
> in Aldor correctly implements some abstract mathematical
> concept ... assuming that the compiler/interpreter and underlying
> computer system perform according to spec.

That's where I think unit testing could be helpful.  I agree that's how
we need to approach it, but that doesn't preclude a) checking this
behavior experimentally and b) someday applying advanced programming
techniques to prove the implementation of the compiler et. al. work as
advertised.  

> Of course this a
> weaker result that what the end-user probably desires, but as
> far as I can see human intellectual limitations making any
> except a level-by-level approach practical.

Sure.  All we can worry about is the Axiom layer, but if we do it right
it will be able to take advantage of eventual other proven layers and
perhaps in time a system will be created that mathematicians will be
able to trust.

> As I see it "regression testing" is really what Tim's CATS
> project can offer - proving that new versions of some package
> or module do not produce newly incorrect results which formerly
> were deemed to be correct. Or simply showing clearly where the
> differences lie. I say "deemed to be correct" because in some
> case the lack of formal proofs and the lack of clear and
> unambiguous understanding of a problem means that what is
> taken to be true at one time *might* change a little over time.

Right.  CATS would effectively be a "top level" functionality test,
while unit testing would be much lower level.  CATS being the more
useful for checking that all the pieces work together as they are
supposed to, and unit testing checking that each piece works as it is
supposed to.

> No, I don't think this is the correct view. It is because of
> tools like lisp that we can even work at this higher level
> at all. We should not be looking to "move the blame" but
> rather thinking in terms of building an elaborate and ever
> higher scaffolding - sometimes shoring it up underneath and
> sometimes building it higher... (: How's that for imagery? :)

Nice :-).  But at least these testing setups will tell us what we need
to shore up.  Think of it as Dtrace for Axiom ;-).

> > d)  Tim, assuming I'm not way off base, would it be possible 
> > to sort of define the steps we want to take to get from
> ? where we are to the 30 years system - e.g. something like:
> > 
> > 1) decide on proof system to use, if in fact that's the way
> > we want to go.
> 
> I am very interested to see how Tim will respond to this since
> very often we have different views although many of our goals
> are the same. :) But I would say emphatically "no" to this. I
> think Axiom needs to be open to the application of several
> different proof methodologies. (notice my emphasis on the word
> *open*).

I think I saw a paper about adapting one proof to other proof systems -
IIRC it was surprisingly difficult.  I should see if I can dig that up
again.

> > 2) integrate proof system with Aldor language and environment
> 
> Yes. In fact there has already been some published research
> on exactly this topic. Check out some of the articles at
> http://page.axiom-developer.org/zope/Plone/refs

OK, will do.

> > 3) outline bootstrapping order in which to document and port 
> > systems to Aldor+Proof Core.
> 
> impractical :(

But isn't it essential?  A proven system will have to build itself out
of proven components, and so doesn't Axiom of necessity have to be
built much as the logic of mathematics itself is built?

> > 4) As migration occurs, document mathematical theory of all levels
> > and requirements of Axiom in terms of support from the underlying
> > lisp.
> 
> Yes. This is very important. It simply must be done if Axiom's
> future is to extend to the 30 year horizon.

Yep.  This is the part I would like to starting thinking about, because
even 30 years might turn out to be a short time given the scope of
mathematics.

> > After a while, with any luck new functionality will be transferred
> > entirely inside Axiom and the lisp requirements will be clear.
> 
> No. This does not make sense to me. As I said, lisp has very
> little to do with this - except as an intermediate language that
> is well-suited to bridging the gap between machine architecture
> and high-level complex programming abstractions.

OK, but there must be some separation between the mathematical logic of
Axiom, and the supporting OS/system libraries/compiler on which it
depends for basic computational functionality.  I would prefer that
that interface be as well understood as possible, and if the supporting
software ever reaches proven stage things could be plugged in rather
nicely - in essence, switched from "assumed" to "proven" :-).

> It is well suited
> primarily because it does not constrain the underlying computational
> metaphor. It is like a very high level machine language. But it is
> *not* a language that is well suited to expressing high-level
> mathematical abstractions - that happens only several levels higher
> up.

OK.  But since in the end all functionality of Axiom rests on those
lower layers functioning properly, wouldn't it be a good idea to at
least have some idea of what we are expecting of them?

> > Of course, doing this robustly probably WOULD take 30 years, but
> > then we would never have to do it again ;-).
>
> I simply do not believe this. If a computer sales person told me
> this about some fantastic new computer system, then I think I
> would very quickly show him or her the door. :(

How about if they presented you with a book of proofs about critical
system functionality and system security? ;-)  You might upgrade it
with better algorithms or cleaner proofs to make it more efficient, but
if the functionality is what you desire wouldn't the basic problem be
solved?

I agree it might not be practical, but darn it I hate the idea of
someone having to redo Axiom somewhere down the road.  Mathematics is
mathematics, after all.

> > I know the more short term goal is to get the beastie fully
> > working at it's original levels, but it would be fun to have
> > some broad steps toward the "ideal" Axiom to start poking around
> > with :-).
>
> Finally.... yes indeed. I agree whole heartedly. I think your
> project with units of measure and physical dimensions in Axiom
> is a very good example. And I like to think of my interest in
> category theory in Axiom in the same light.

I agree.  Units and dimensions is a bit more of a "practical" project
in the sense of wanting to use Axiom's abilities in the sciences, but I
will try my best to do it the "right way" and hopefully, if proof logic
comes to Axiom, it will be straightforward to port the units pamphlet
into the new world :-)  Category theory, on the other hand, is
fundamental to what Axiom is :-).  

Cheers,
CY


                
__________________________________ 
Yahoo! Mail - PC Magazine Editors' Choice 2005 
http://mail.yahoo.com