3

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.

enter image description here

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

12
  • 4
    Possible duplicate of Theoretically bug-free programs
    – gnat
    Sep 14, 2017 at 12:37
  • 4
    How would you prove that the contracts themselves didn't contain errors? Also, how would you make your contracts rigorous enough to cover every possible edge case? Wouldn't you essentially be recreating your tests in contracts at that point? Sep 14, 2017 at 12:51
  • Not to mention the inevitable slowdown as your contracts are tested and verified every call rather than once at test time. It is possible to introduce incorrectness due to timing lag and the inability to meet performance criteria while still remaining functionally correct. Sep 14, 2017 at 12:55
  • @RobertHarvey Yes kind of creating tests again, by saying contracts. Does it look like Test Driven Design with this approach? Sep 14, 2017 at 12:55
  • 5
    As Donald Knuth said: Beware of bugs in the above code; I have only proved it correct, not tried it.
    – mouviciel
    Sep 14, 2017 at 15:21

6 Answers 6

10

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.

9
  • How would the tests help us know the correctness of solution(code), in situation where design spec derived from the requirement is wrong? Sep 14, 2017 at 12:59
  • By demonstrating that the software fails to meet the requirements. Sep 14, 2017 at 12:59
  • Software failing to meet the requirement is observed, but tests are not helping us know that Sep 14, 2017 at 13:01
  • 4
    Well, to be productive as a software developer, you have to buy into the idea that tests (of any kind) have some value. If you don't believe that, there isn't anything that I say that's going to change your mind. Sep 14, 2017 at 13:02
  • Requirements without acceptance tests are not requirements at all; they are wishes. Not quite true, requirements must be verifiable. If they are not verifiable, then they are wishes.
    – Robbie Dee
    Sep 14, 2017 at 20:54
5

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.

4

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.

2

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/

1

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.

0

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.

3
  • "not possible": while it is true that the tools for automating proofs to some degree have been neglected relative to other tools, such as basic compilers and interpreters, there has been some progress. One invariant typically provided by higher level languages is freedom from heap corruption and stack corruption. Of course this depends on proof of implementation, but it is progress of a sort. The rise of functional languages such as Haskell is also a trend toward using languages that are more proof-friendly. Sep 15, 2017 at 16:23
  • You are right, I tried to keep my answer brief because you can always digress into many different directions. There are algorithms that are easy to proof, and that are difficult to proof. Proving that whole commercial system is bug free is infeasible or considering that it's ever changing - virtually impossible. This is what I wanted to express, Thanks for your explanation @FrankHileman
    – Greg
    Sep 17, 2017 at 14:00
  • Although I agree with your statement, I don't like that this argument is often used to dismiss even informal, easy proofs of low-level code. Those that take the time to at least determine system invariants, and check pre-conditions and important post-conditions, at run-time, generally write more robust programs. This does not eliminate the need for testing, but the main deficiency are the tools. Sep 18, 2017 at 16:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.