On Tue, May 26, 2009 at 3:55 PM, rjf <fate...@gmail.com> wrote: > > Disregarding the obvious " marketing fluff" of Wolfram's statement, it > seems to me plausible that some programs are more likely to be correct > (at least in well-understood basic components) than some theorems' > proofs. Here's why. > > A program can be run on test data. > A program can sometimes be analyzed to a 'higher level' abstraction, > namely a programming language, whose semantics are agreed upon and can > be used to synthesize "theorems" that can be used in proving programs. > That is, subroutines are susceptible to re-use as though they were > "axioms". > > For example, assume I have a program M0 that can multiply 2 > polynomials of degree 0. > > I can write a simple program M "by induction", to multiply two > polynomials A, B where the polynomial A is of higher degree , n>0 by > observing that if A=(a*x^n+ A2), then A*B is (a*B)*x^n + A2*B, and A2 > and B are of lower degree. > By hypothesis, M (or M0) can be used for these two subproblems. > > Testing such a program against known data gives a certain level of > confidence. If the program works for degrees 0,1,2 it is unlikely to > break at degree 203. Though you could imagine that in some > programming language in some operating system on some hardware with > some limited amount of memory etc etc, something could go wrong go > wrong go wrong..
A few weeks ago we had a strange bug in a prerelease version of Sage, where it would square univariate polynomials (modulo the cube of the prime 10007) and work fine for degrees up to about 3000, then suddenly get everything wrong when the degree exceeded about 3000 (on all operating systems and hardware) -- see http://trac.sagemath.org/sage_trac/ticket/5817. We only discovered it because we had a test case involving computation of the matrix of Frobenius on certain Monsky-Washnitzer cohomology groups -- the input and output of the computation were very simple, but the intermediate steps involved arithmetic with univariate polynomials of large degree. The bug was sufficiently subtle that it wasn't picked up at all by the responsible library's very extensive test suites. William --~--~---------~--~----~------------~-------~--~----~ To post to this group, send email to sage-devel@googlegroups.com To unsubscribe from this group, send email to sage-devel-unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-devel URLs: http://www.sagemath.org -~----------~----~----~----~------~----~------~--~---
