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
