...[snip]... > > In regular mathematics it is standard practice to fully document, that > > is, show the complete proof of your findings. In computational maths > > we do not do this. There is no particular reason why we don't except > > that it is not the expected behavior. > > Unfortunately this is rarely true these days. In regular mathematics > it is now very common for there to be large leaps between steps. > Usually the more advanced the mathematician the less detail that is > expected. Graduate students spend a lot of time filling it in. > > But your point regarding computational mathematics is spot on. It is > very common to find code completely undocumented in any way. There is > a substantial disparity in attitudes here.
What concerns me is the long run. We are at the very beginning of a new science of computational mathematics. The early systems are the "newton's notebooks" of this science. Most of them are locked up in companies (MMA, Maple, Derive, Macsyma, etc.). But companies die and take their software with them, for example, Macsyma. (For company deaths see the last few minutes of: http://www.ted.com/talks/geoffrey_west_the_surprising_math_of_cities_and_corporations.html If we are to have a firm foundation for computational mathematics it is necessary that we begin to build the citation trail of algorithms available in a public, published way. Why are we wasting time and effort reinventing algorithms? Why can't I find executable algorithms along with their theory? Why can't I attend a talk, download the literate paper, and execute the algorithm while the talk is ongoing? > > When I began my massive rewrite of flint from scratch I decided that > each function would have a complete description and justification of > the algorithm (if not well-known) in an associated text file, with > references and proofs if necessary. Sebastian Pancratz came along and > saw these text files and decided to write a parser that automatically > turned them into pdf documentation! Excellent! Although I'd much rather follow Knuth and have a literate document I find it outstanding that you have created these. Can you point to a URL as an example? > > > > > We could raise the bar of expected behavior by having algorithms fully > > explained in the source code along with citations of theory sources. We > > could include a section on limitations, boundary conditions, examples, > > assumptions, and test cases. This is not as challenging as it sounds > > if it is done by the original author. It is extremely hard to recover > > or discover this information after the fact. > > To a good extent this is done in most of the Sage library. I agree > this should be the expected standard. I am unaware of this, which is clearly my fault. Can you point to an example you consider literate? > > Again I have to credit Sebastian Pancratz and Fredrik Johansson here > for raising the standard in flint. I thought I had been producing > beautiful code until Sebastian started rewriting some of it for > me. :-) > > > > > Knuth proposed the idea of "literate programs" which combine the > > actual source code with the human language text as a single document. > > The document re-arranges the source code for ease of explanation and > > includes the usual paper sections on background, theory, along with > > a bibliography citing prior (literate) work. (See Queinnec, Christian > > ``Lisp in Small Pieces'' ISBN 0-521-56247-3 for a literate example) > > My favourite example of this is Jonesforth. I highly recommend anyone > who has not read this program to do so immediately. It is one of the > most beautiful documents you can obtain for free. And you get yourself > a Forth implementation at no extra cost. All page references to Jonesforth seem to time out. I am writing a similar document for the Clojure language. The literate document contains a full implementation of Clojure. Unpacking the document creates a Clojure REPL and a PDF of the documentation (well, as far as it has gotten at this point). source: http://daly.literatesoftware.com/clojure.pamphlet pdf : http://daly.literatesoftware.com/clojure.pdf > > I don't personally do literate programming in the sense you intend it, > with rearranged code so that it reads more naturally. But for very > complex and touchy pieces of critical code I sometimes add formal > justifications for every line of code. A good example of this is the > bitpacking code in flint. > > > > > We could take small steps in this direction, possibly by hosting a > > "literate program" track at conferences or workshops to encourage the > > more literate among us to show examples and build up the technology. > > I could certainly imagine a talk being constructed around an actual > program. I might try this one day and see how it goes. I would like to see Sage have some small step in this direction but I have no idea where to start. I know next to nothing about number theory so I couldn't begin to reverse engineer the algorithms. I am also not well versed in the Sage build process so I don't know where to integrate literate tools into the process. > > > > > Raising the standards for published mathematical software will help > > us all in the long run. We can look forward to a time when we can > > read, understand, and cite particular Pari and Sage algorithms which > > are their actual implementations in literate form. > > > > It's not the only important step that needs to be taken though. > > My epiphany regarding automated program checking came when I > serendipitously encountered a fantastic book on Prolog on the exact > same day that I sat down to implement Damas-Hindley-Milner type > inference for an interpreter I have been writing. I marvel that a 20 > line implementation of the unification algorithm saves me so much > hassle. After this little epiphany I have not had any problems seeing > the future. Type inference and unification have been around for ages, > but I feel like someone who has been in a time machine and returned > and who has to sit around and watch the inevitable development of the > compiler technology that I have already seen. Progress feels like a > slow motion replay. Ah, indeed. Another direction is the development of automated proofs. I don't know about Sage but Axiom has an algebraic "scaffold" that looks like it will allow us to attach definitions and theorems (e.g. around Groups, Rings, Fields, etc) and then prove the algorithms that, say Ring, implements. I have had many discussions, some with the people at UTexas, working on ACL2. There are other efforts (e.g. COQ) in this same direction. The root question is "How do we connect mathematical theory to computational mathematics in a rigorous, automatable way that can be published and peer-reviewed?". The task is too big and the goal is too distant for a single leap. It would be better if we could begin to have something like a Sage "track" (like HICSS tracks), that calls for, reviews, and accepts literate software. Each example paper could slowly raise the standards of good practice. Flint might be a good place to start. Perhaps there is an ACM connection to this effort. (I am no longer an ACM member though). ACM might help sponsor some of the presentations. NIST is also a potential partner as these algorithm papers could become standards. Oak Ridge National Labs has a numeric library interest and might be convinced to help fund a literate form of the library. Sage has a reach and connection with a large number of academic researchers. It would certainly help a tenure review if the software algorithms were in literate, peer-reviewed paper form. This might help get tenure-track people more involved in the creation of software since it seems that "only papers" count in the tenure process. In any case, if the papers were literate then it would be clear who, what, and how to cite prior work. Literate Pari papers would be an obvious example. 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
