Bill Hart wrote:
Why is this entire thread not on sage-flame? What does software
engineering, documentation, test code, etc. have to do with "Creating
a viable free open source alternative to Magma, Maple, Mathematica and
Matlab."?
Despite what appears to be competitive badgering I really do want Sage
to succeed.
But I don't want Sage to spread the impression that mathematical
software can't be trusted.
I badger because computational mathematics is my chosen field of study
and I feel it is
*vital* to raise the standards to professional, high quality,
trustworthy levels. If Sage is going
to be the M$ of mathematical software, will it also convince everyone
that math software
just gives highly questionable answers? Every program makes mistakes but
hand-waving
about "it's not my problem, it's the upstream code" gives the whole
field a bad reputation.
And I very much care about that. This *isn't* software, this is
*computational mathematics*.
If advocating such project goals is considered "sage-flame" material
then we all lose.
...[snip]...
Why attack Sage. It is what it is. Why defend it. It certainly didn't/
doesn't get everything right. One thing is for sure. Whatever is wrong
with Sage, it is almost certainly too late to fix it. Whatever is
right with Sage certainly made it popular.
*sigh*
If you want to make Sage seriously innovate to solve one or more of
the above, you need a *large* group of like-minded volunteers who can
help you. You won't do it on your own, no matter how many years you
work, nor how hard.
Many of the things Tim and David say resonate with me. I'd really,
really love a tremendously efficient, well-documented, reliable, Open
Source mathematical project. Having seen how insanely difficult even
just goal number 1 is for just the domain of arithmetic, I honestly
think we haven't got a chance. Not ever. The expertise don't exist in
sufficient quantity. And even those with the expertise, don't have the
time. So, looks like we are stuck with what we got.
Re: "don't have the time"... Unlike any other software effort, programs
like Sage are timeless.
The integral of the sin(x) will always give the same answer, now or 30
years from now. Any
one individual does not have the time but "the project" does, assuming
it lasts. Would you
read a mathematics journal with the editorial policy "we'll print
anything because we don't
have the time?".
By the way, does anyone know what the current state of program proving
is? How does this work? Does one write the proof by hand then
formalise it in code in a formal system until it "parses"? Can someone
give me some references on this. I am genuinely interested. I've read
some comments about SML being good for program proving (why?), and
that the Haskell type system amounts to giving a "proof" under some
circumstances. But it is baking my noodle how any of this has anything
to do with proving programs, especially in mathematics. The "monad"
idea in Haskell gave me some hope, because it sounds mathematical, but
I simply didn't understand it, at the end of the day.
See http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
and http://userweb.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#top
and http://coq.inria.fr/a-short-introduction-to-coq
The first one shows that writing programs and proving programs have a
correspondence. The second one shows ACL2 which is basically a way of
writing program proofs in lisp. The third one shows COQ which has a very
strong connection between mathematics and types.
In systems like Maxima and Axiom it would be possible to embed ACL2
directly into the system (lisp is lisp after all) and perform the proofs
inline.
Given the mathematical definition of a Ring and a function on the Ring
elements you could prove the function correct. For Axiom this is part of
the stated long term goals of the project.
On the other side (at the machine level) there is a program called FX, that
is, Function Extraction. FX grew out of the work by Richard Linger,
Harlan Mills, and Bernard Witt. It is being constructed at the Software
Engineering Institute. FX reads machine language, extracts the semantics,
and composes the instructions into blocks of behavior. You can't fully test
a program but FX covers *all* of the program behavior so you can identify
failing cases. See
http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/Man75586.pdf
(disclaimer: I am one of the authors of the FX technology)
"Testing programs" is as ineffective as "testing theorems".
No matter how many examples you create, you don't have a proof.
Tim Daly
--
To post to this group, send an email to sage-devel@googlegroups.com
To unsubscribe from this group, send an email to
sage-devel+unsubscr...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/sage-devel
URL: http://www.sagemath.org
