Is there no substitute for testing?

Question

Entscheidungsproblem placed a challenge in 1926,

Can we write an algorithm that checks to see if a proof can be solved without actually doing the proof?

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"

So, it implies, that a working program(algorithm) as a proof of a solution to a problem, makes the problem say computable.

But testing that proof actually verifies, if a program actually satisfies its requirements and performs the desired operations, then working program is considered proof of solution.

---

Below is the typical use case template with requirements and acceptance parameters. Under Agile SCRUM framework, we have user story for the same.

Can't a solution be designed with an approach like Design by contract to create bug-free solution? In order to avoid testing.

Answer 1

There are languages like Haskell that have very sophisticated type systems that can eliminate certain classes of errors. I have heard (though not experienced it myself) that if you can get your types correct, a Haskell program will often run correctly on the first try.

That said, no, there's no substitute for testing. The reason is that every non-trivial software system also has a requirements specification, and you need testing to prove that the requirements have been met. Requirements without acceptance tests are not requirements at all; they are wishes.

Answer 2

Thought I know little of the subject I think you are mixing two differents concepts :

• Not being able to solve a theorical problem
• A bug

Your quote is about solving a theorical problem however you're asking for a bug-free programs. Usually solving a theorical problem don't take into account "physical/real" problems of computering. Of course when you write an application for a customer, if your solution runs into one of those physical problems you will have what we call "a bug" even if your algorithm theorically works. So a bug can be :

• one that does not solve the specified problem properly (not at all, edge cases,...)
• Time performance : your algorithm works but in production takes way too much time to run.
• Memory consumption : OOM errors
• Space performance : you write data and you have not space anymore.
• Number Precision (Floating point ...) ending up with wrong results, dividing by 0,...
• ...

To conclude : at best you could prove that you are able to tell what an algorithm will do in a perfect world where all of those "physical" matter does not exists, but no more.

Here is a DailyWTF reference on the matter.

Answer 3

In a very broad sense, there are substitutes for testing and you have suggested one. As in real life, however, substitutes are often inferior to that which they replace.

The question you are asking has a long history in philosophy and in that debate, empiricism has become the dominant belief. It is the core of science, as we understand it now.

A great scientific philosopher of his day, Empedocles created the emission theory of vision. This theory held that vision was the result of rays emitted from the eyes. It was logically sound and was considered correct for centuries by really smart people such as Plato. But we now know that this is completely wrong. When you use pure reasoning to come to a conclusion, you must make some assumptions; there is no way around it. And it's those assumptions that can lead to failure.

Let's say that you can use design by contract to 'prove' a correct solution and use some tool to create software. You are assuming that the tool has no bugs. Walfrat enumerates a number of other possible pitfalls. You cannot avoid that the proof of the pudding is in the eating.

Answer 4

Yes, this type of software is written for avionics and other areas where regulations require it. Design by contract is not exactly the way it is done, but for the type of software you are probably writing, it is a good approach. You create a hierarchy of proofs:

• Preconditions, postconditions, and invariants for the lowest level types.
• You must be able to prove the correctness of the lowest level types: ideally using automated tools, not by hand. This means you do need a contract language.
• Higher level types have higher level invariants, based on the proofs provided by the lower level types.
• At the application level, you can prove application invariants.

With the correct tools, you can put together previously proven correct components to create proven programs. However, you might not think of this as writing software any longer... you may be using only graphical tools.

Here is an interesting project which is relevant both to your question and to the types of vulnerabilities continually introduced using typical software development (i.e. tests instead of proofs): https://project-everest.github.io/

Answer 5

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.

Answer 6

So, it implies, that a working program(algorithm) as a proof of a solution to a problem, makes the problem say computable.

Yes, if you have a program, which solves a problem - you proved that the problem is computable.

But testing that proof actually verifies, if a program actually satisfies its requirements and performs the desired operations, then working program is considered proof of solution.

Well - you program has to work correctly for different inputs (especially edge cases). And checking if your program returns expected output to different inputs is... testing.

And proving that your program works for every input is in most cases not possible... or at least very hard. So testing is just more feasible approach.