On 30 Aug, 03:09, Tim Daly <d...@axiom-developer.org> wrote: > 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.
Whilst I certainly understand that you want Sage to succeed (I do too) and I understand your concerns (I share them), I am much more circumspect about what is actually possible. > > 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. I'll be blunt. I don't think Sage is ever going to do this. It was once stated that having code accepted through the review process into Sage should be considered equivalent to having a paper reviewed in a top journal. Whilst I once supported this as a goal for Sage, I no longer support it. Knowing what I do now, as opposed to 9 months ago, say, about coding, software, programming languages and even Sage, I cannot take this seriously any more. Sage is not designed to "raise these standards" and nor do I think it should be a project goal to do so. It would be fatal to the project. > If Sage is going > to be the M$ of mathematical software, will it also convince everyone > that math software > just gives highly questionable answers? I hope so. Because many people are currently under the illusion that it does not. The reason Sage is becoming the M$ of mathematical software (not quite the analogy I'd make, but I think I understand your point), is that it has stuck to some very important (social) rules, right from the start: 1) Anything is possible in 24 hours. Absolutely anything at all. Once you start putting constraints on me, then less is possible. So if I am not constrained, and I can do whatever I need, to satisfy you, then I can do it in 24 hours. And why wait 24 years, when I can do it in 24 hours. The time it takes to get something done, even something useful, depends only on how many constraints you add. 2) If some problem is exposed, there is no need to develop some complicated, time consuming methodology to avoid the problem in future. Simply work harder. If there are bugs, patch them. If there are missing features, send me a patch. 3) Mathematicians respond very well to challenges. If you really want something done, tell everyone it is really, really hard and you don't think anyone will be able to do it, but you'd like to see someone try. Add that you really think it will be nearly impossible. Make sure you underline the fact that it is really, really hard, and no one has succeeded so far. Keep repeating this. Eventually someone will take the bait. This especially applies to problems all the experts agree is hard. But here you need *young* players, who *know* the experts must be wrong and that *they* will be the one to solve the problem (often they are right). 4) If anyone does *anything* at all, make a big fuss about it and email everyone you know who might be even tangentially interested in what they have done. Under all circumstances encourage them to do more. > 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. I don't recall who wrote that comment above, and I'm not going to check. But they'll have a hard time living it down. I assume they were not serious, or not thinking. Anyhow, it has been thoroughly debunked. > And I very much care about that. This *isn't* software, this is > *computational mathematics*. Ah, that non-academic pursuit called *computational mathematics", which everyone would like to become a hard core, well-funded academic subject. That is not going to happen because of Sage. That will happen because of a single individual who has a brilliant new idea that puts the whole subject on a solid theoretical footing. That new idea is going to have to be absolutely brilliant. It will make our petty squabbling look just that. The fact is, none of us has had that big idea. It's still out there. Literate programming, using more "scientific" languages like Lisp, theorem proving, program proving. None of these is the solution. Sage surely has nothing to offer in this regard. It is a social success, and it is giving a lot of people interesting things to do. As a community, it is very valuable to be part of. The software also happens to do a *lot* of stuff, even useful stuff. It is very successful, but not in the sense you want it to be. That idea is still waiting to be had. Of course this "single individual with a brilliant new idea" seems to contradict what I say below about needing a large group of volunteers to help you meet your goals. Maybe the two are not talking about the same thing. Maybe they are and don't actually contradict one another. I haven't decided yet. > > If advocating such project goals is considered "sage-flame" material > then we all lose. It's only sage-flame material in that it misses the fact that the community simply doesn't seem that interested in these goals. > > ...[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* Seriously? Do you think there is a missed opportunity here? Do you really think this crowd should be gainfully employed working on a project with different goals? Do you think they would? > > 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. The problem is, that socially, the project will not continue to succeed, unless it appears to meet the goals of those involved in the project. Go ahead and prove me wrong, but I don't think any amount of "advocating" is going to fundamentally change the goals of all those people. Nor is it going to rewrite those 500,000 lines of code. > Would you > read a mathematics journal with the editorial policy "we'll print > anything because we don't > have the time?". I don't believe the editorial policy, nor the peer review process produces more accurate mathematical papers any more than it produces bug free software. I am not under any illusions about the correctness of the published literature any more than I am about the correctness of code in Sage. > 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. > > Seehttp://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence > andhttp://userweb.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#top > andhttp://coq.inria.fr/a-short-introduction-to-coq Thanks. I had heard of coq. I will devour the other references with gusto. Some computer science type question bothered me for 9 years, until I finally saw that it had been solved. I hope this one doesn't keep me occupied for as long. I cannot get it out of my mind. > > 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. I read an example of this earlier this evening. It was on using Lisp to prove the complexity of some sorting algorithm or something. I was pretty unconvinced, however, that this was anything more than using Lisp as a glorified calculator to symbolically prove the induction required to prove the complexity. Nonetheless, I nearly swallowed my food the wrong way when I realised that Lisp separates symbols from the values they are bound to. And I couldn't shake the feeling that the secret to program proving lay here somewhere. I hope your references might lead me to be able to understand why I feel that. Somehow I also have the feeling that the fly-in-the-ointment with this sort of thing turns out to be arithmetic. Sorry I can't put this gut feeling into words that make sense. So I won't try. > The third one shows COQ which has a very > strong connection between mathematics and types. Ok. > > 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. Of course, Though it sounds like I can just use Lisp, and don't need axiom or maxima. > 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. Just out of interest, what do you mean by prove correct? Do you mean, prove the algorithm correct, or the implementation, or the complexity, or that the function means what you agreed it means according to some contract? > > 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. > Seehttp://daly.axiom-developer.org/TimothyDaly_files/publications/sei/Ma... > (disclaimer: I am one of the authors of the FX technology) Sounds interesting. I will take a look. Thanks. > > "Testing programs" is as ineffective as "testing theorems". > No matter how many examples you create, you don't have a proof. Yes. This is the level at which people should have confidence in (current) mathematical software. > > Tim Daly Bill. -- 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
