Before we begin, I think it's worth mentioning Philip Wadler's "Propositions as Types", which gives an excellent overview of the early history of computability theory with an emphasis on first-order logic. There's a video presentation of this as well. I highly recommend anyone with an interest in this topic watch the video and read the paper.
Alan Turing reduced his Halting problem to this problem, by saying in his paper: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0"
Yes, if the Entscheidungsproblem is computable then the halting problem is computable. The halting problem has been proven to be uncomputable, so therefore the Entscheidungsproblem is uncomputable. In other words, a general algorithm to prove whether any arbitrary program is correct or not does not exist. However, that does not mean there do not exist algorithms to prove whether some programs are correct or not.
So, it implies, that a working program(algorithm) as a proof of a solution to a problem, makes the problem say computable.
If by "working" you mean "correct" (including the halting condition), then yes, we can say that a provably correct algorithm that solves a problem is proof that problem is computable. However, how do you know a program is correct? We know there can not be a general algorithm to prove its correctness. That leaves us with two options:
- We can (try to) do the proof ourselves. However, the uncomputability of the Entscheidungsproblem implies that some things are not provable. If we run into one of these problems, formal proofs are a dead-end. Furthermore, there's no way (in general) to even know if we are trying to prove something that is unprovable. So we could spend any amount of resources towards a problem we will never solve.
- We can (try to) express the program (and the problem) as a subset of the problems for which we have an algorithm to do the proof automatically. Note, however, that we must then prove the prover correct. So, ultimately, someone has to do a proof by hand at some point.
Even when theoretically possible, both options are very time consuming. If we are unable (or unwilling) to do either of the above, then really testing is all we are left with. By verifying correct results are produced for at least some of the possible inputs, we approximate a comprehensive proof to some extent.
In addition, there are many practical aspects that formal proofs of correctness do not address. A few of them are:
- Time and space performance. It doesn't do us any good if our provably correct program does not compute a result before the heat-death of the universe. Or if it fails due to stack overflow. Or if it exhausts main memory or some other resource. In order to be practical, we would need to prove these properties as well. Theoretical correctness per se is not enough.
- Did we express the problem correctly to the automatic proofing system? I.e., are we actually solving the problem we think we are solving.
- Are we solving the right problem? A provably correct program is of no use if it solves the wrong problem.
- Whenever the requirements change, the problem changes. So any change requires a reformulation of the problem and a new proof of correctness.
I think this is why there has been relatively little push in the industry towards formal proofs. However, that does not mean we never use proofs. For example, static type-checking is used to prove a program is well-typed. This can eliminate a certain class of errors, but it cannot by itself rule out all errors.
In some cases, it is possible to prove a program correct by verifying it produces the correct result for all possible inputs. In those cases, testing itself can actually be the proof of correctness. Most of the time, though, the input space is much too large (or even infinite) for such a strategy to be practical (or even possible). So in general, it is impossible to prove a program correct via testing.
However, we can prove that a program is not correct via testing. This happens by observing a failure in a test. So the utility of testing comes down to having "good" tests that cover "useful" properties, and having "lots of them". We can write tests by hand, but not very many. If we have well-defined properties we wish to test, we can use tools such as QuickCheck to automatically generate many tests for us.
So I would say that design-by-contract, in general, does not replace testing but rather compliments it.