A bigger problem is that a program without source code available becomes thing of the past faster than one wants. Imagine Leonard Euler referring for his proofs to a computer running a very old version of Ma*... Even if he gave Ma* scripts for his computations, no modern computer would be able to run that Ma*, even if by some miracle you can get hold of a binary of that Ma*...
On Nov 5, 1:38 pm, rjf <fate...@gmail.com> wrote: > On Nov 4, 5:17 pm, Jason Grout <jason-s...@creativetrax.com> wrote: > > > > > > > > > > > On 11/4/10 6:56 PM, William Stein wrote: > > > > On Thu, Nov 4, 2010 at 4:32 PM, Jason Grout<jason-s...@creativetrax.com> > > > wrote: > > >> On 11/4/10 6:12 PM, rjf wrote: > > > >>> 1. can you prove a program correct without looking at its source code? > > >>> answer: yes, sometimes. > > > >> I'm really curious. How would you do prove a program correct without > > >> looking at its source code? (I assume "prove correct" means that you > > >> guarantee that a certain set of inputs gives a corresponding certain set > > >> of > > >> outputs, assuming a perfect computer, compiler, no cosmic rays, etc.) > > > > Here's a trivial example. Suppose you have a program that is (1) > > > deterministic, and (2) has only finitely many inputs. > > > Then you could prove it correct by trying all of the inputs :-) > > > I guess I was thinking that information like "the program is > > deterministic" involved looking at the source code. Sure, if you're > > willing to trust someone saying that, then why not trust them saying, > > "look, the program is correct, all right?" After all, apparently *they* > > looked at the source code. > > > No, I was imagining the situation where you are given just a black box > > function call, and from that you were supposed to prove the program was > > correct. > > > Jason > > WS is right. Some programs, e.g. sqrt(16-bit-number) are reasonably > easy to > prove correct by trying all possible inputs, and have been tested that > way. > > Can one prove that such a program is deterministic? Perhaps one can > force > it to be deterministic by running it in a virtual machine with no > memory, input, or > output, if you wanted to be a stickler. > > I don't know what it would mean for a computer to gain an increased > depth of > understanding; it sounds like something that happens with humans. > Computers > store data sort of all at the same depth :) > > Does a human seeing source code gain an increased depth of > understanding of a computation? It might happen. > > Does the lack of availability of source code for a program mean it is > unacceptable > to publish the results of that program in a journal? I think not. > > Is it nice to release your program and data along with your article? > Sometimes. > I try to do so. > > RJf -- 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
