Hacker News Reader

Comment by crntaylor | Hacker News Reader

I don't agree with this statement

  "It is not sufficient merely to prove a program correct;
   you have to test it too."

It is sufficient to prove a program correct - as long as your proof is not faulty! The problem in this case was not that the program had a bug despite being proved correct. The problem was that the 'proof' was not a proof at all.

Machine ints are not mathematical integers. Floats are not real numbers. You can't prove things about programs that use ints/floats without taking these things into account.

Of course, the question of how one knows that a proof is correct is still left open - but that's a metatheoretical argument that it might be best to leave aside. I suspect that most faulty proofs are faulty for pedestrian reasons (incorrect type assumptions, failing to deal with null/NaN etc) rather than high-falutin' concerns about the validity of first-order logic.

View on HN

Computers are now complicated enough for Computer Science to have turned to some extent into an empirical science - it is impossible for a single person to have in their head everything that goes in a typical computer, operating system, compiler and so forth, so one is often forced to resort to experiment to find things out, it's no longer a theory where you can just reason things out, maybe it never was one in fact, because many simple imperative programs are so complex to reason about.

In empirical sciences, you not only have to have a mathematically valid theory, but you also have to check if the theory fits reality by making predictions and experimentally checking them with the real world. It's the same now in Computer Science, there are so many places where theoretical assumptions might deviate from reality that having a proof is not enough. In fact, you have to have those assumptions to make things mathematically tractable. Imagine mathematicians or computer scientists re-proving real analysis theorems using floating point arithmetic...

In other words, your vision of proofs being enough as long as all the assumptions are part of the theory, seems utopian to me. In fact, even some of the most devoted advocates of correctness proofs have admitted this:

http://www.gwern.net/docs/1996-hoare.pdf

> Imagine mathematicians or computer scientists re-proving real analysis theorems using floating point arithmetic...

Mathematicians and computer scientists do prove theorems about floating point arithmetic! For example, the most widely-cited floating point reference contains no fewer than fifteen theorems about floating point:

http://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.ht...

Or here's a presentation about representing functions with their Taylor expansions using floating point arithmetic, providing strong error bounds on the result of adding or multiplying two functions represented in this way:

http://perso.ens-lyon.fr/nathalie.revol/talks/ICIAM07.pdf

I agree that many proofs in computer science are harder than proofs in mathematics, because you can't deal with idealizations - you always have to think about the machine. But unlike empirical sciences, we have access to the design of the machine. We know what many of the axioms are. Formal reasoning is valid for a far larger part of computer science than for the natural sciences.

I'm not going to argue that proofs are a panacea for every situation. But I also don't categorically reject them in the domains where they can be usefully applied.

I know there are theorems about floating point, that's missing the point, what I am saying is that the theories most useful for doing reasoning are often nearly impossible to formulate if you would like to include in them a lot of messy details of something like floating point, just as one example. What happens instead, we reason using nice idealized theories, and then we experiment to asses the gap between theory and reality.

I am completely a fan of theory and proofs, but the point of the quoted comment is that there is an empirical component to software development too, and your original comment seemed to question it.

A theory, no matter how well defined, will never, ever, precisely match reality.

Testing is not optional. Why are you implying you can proof your way around this? A "proof" is useful for some problems, but I'll take very rigorous real-world tests over a proof any day.

I do agree with the quoted statement. I have a lot of experience with machine-verified proofs (in a language called Coq). Even though Coq guarantees that an accepted proof is correct, you still can't necessarily trust it, because your formal model of the program may be not accurate enough, or your statement of correctness is improperly stated.

In this case, it seems like their proof was correct with respect to their model, but their model did not match up with reality. No amount of formalization will ever be able to solve this problem completely. I think the role of testing in this context is to make sure your formalization of the problem says what you meant to say about the world that you meant to refer to. Input/output examples (aka, tests) are a great way of convincing yourself of this.

This hinges on the definition of "program". The OP did not say "algorithm", which is often assumed to be something on paper rather than a piece of working code in $LANGUAGE. I believe that nearly anyone will assume that a "program" is something tangible, something that a computer can run.

So, the OP did not prove the program correct, but he did prove the underlying algorithm correct.

>It is sufficient to prove a program correct - as long as your proof is not faulty!

This is unquestionable truth. Proof:

Proposition A(X): X is true in theory

Proposition B : For all X such that A(X), X is true in practice

Theoretically, there is no difference between theory and practice. ... (1)

Theoretically, statement B is true. [using (1)] ... (2)

Therefore, B is true in practice. [using (1) and (2)]

QED.

theory is very often contrasted to "practice" [...] a Greek term for "doing", which is opposed to theory because pure theory involves no doing apart from itself. [1]

[1] http://en.wikipedia.org/wiki/Theory

I would change it to "It is not sufficient merely to prove AN ALGORITHM IS correct; You have to test your implementation as well" ...

Not that it detracts from your point, but the phrase is a reference to a famous Knuth quote:

http://www-cs-faculty.stanford.edu/~knuth/faq.html (see the last question)

Reply on news.ycombinator.com