I sent a note to boothby, asking that he forward it to sage-devel if my cc didn't work, which it didn't. But he didn't forward it. That's ok, I guess. In the unlikely event that you want to read the whole back-and-forth, please contact me or Tom.
But there is one point that I think is worth discussing, and that is Tom's contention, not entirely novel, that the reason for open- source :. "It's about proof; you can't prove a result with Mathematica, since one can't readily inspect the source." my reply, which you may chew on... You assume that seeing the source code is either necessary or sufficient for a proof. Can you prove that? Read the paper by Demillon,Lipson, Perlis, about proofs and social processes. How do you know that a program written in python, is correct unless you prove the compiler/interpreter is correct, the hardware it runs on is correct down to the gate level, there are no hardware glitches, the memory is proved, etc. And why would you, a human believe the proof if it were written down on 2,000,000 pages? And since your system has components in other languages like C, and Lisp, and is compiled on various different compilers, on various different computers, you would have to redo all the proofs for each environment. And when the C compiler was updated, or a new Pentium came out, prove it again. I recall stories that claimed, a few decades ago, big integer arithmetic software testing programs were used to find hardware bugs in supercomputers. And you know about the intel divide bug fiasco. a citation for demillo etal http://portal.acm.org/citation.cfm?id=359106&coll=portal&dl=ACM the abstract: It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design. --~--~---------~--~----~------------~-------~--~----~ To post to this group, send email to sage-devel@googlegroups.com To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/sage-devel URLs: http://www.sagemath.org -~----------~----~----~----~------~----~------~--~---
