4
$\begingroup$

I have seen that programmers test their programs often to find out if there are bugs. But is there a way to prove mathematically that a software has no bugs? If it is possible, why it is used so seldomly? For example, Linux kernel has many bugs.

$\endgroup$
4
  • 2
    $\begingroup$ To my knowledge, there has been limited industrial use of theorem provers like ACL2 to prove software correct since the mid 1990s. This was initially limited to specialty code like portions of the microcode inside microprocessors. At the time, microcode was sometimes non-trivial to update and also fairly small (1000 lines of code or less). Back then it took an expert (usually a mathematician) several months to formulate the proofs, with only the checking being automated via the theorem prover. In other words, it was an expensive undertaking. I do not know what the current state of the art is. $\endgroup$
    – njuffa
    Dec 4, 2021 at 11:04
  • 2
    $\begingroup$ Warren A. Hunt, Matt Kaufmann, J Strother Moore, and Anna Slobodova, "Industrial hardware and software verification with ACL2," Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375.2104 (2017): 20150399 (online) $\endgroup$
    – njuffa
    Dec 4, 2021 at 11:23
  • 1
    $\begingroup$ "If it is possible, why it is used so seldomly? " Simply because it's extremely expensive. It's doable to some extent for super critical software (e.g. space), but if it was necessary for software like operating systems, we would still be using the technology from 30 years ago (it would be very reliable though). $\endgroup$
    – Erwan
    Dec 4, 2021 at 11:40
  • $\begingroup$ First formally define the definition of a bug $\endgroup$ Dec 16, 2021 at 5:09

5 Answers 5

2
$\begingroup$

"In theory, theory is the same as practice, but not in practice." (Often attributed to Yogi Berra).

Let me try to explain why the problem is hard - harder than it seems. Some things can be formally verified, others not.

First, a piece of software to be verified is part of an ecosystem. It interacts with other software that may not be verified. Moreover, it depends on other systems (software and hardware) down to the silicon level. There may be unfound issues both at a given level and in the software/hardware stack on which it depends.

Second, software can be very complex. Humans have limited ability to see all the nuances that might be involved. In some areas math and math-like processes can help, but people also make mistakes. It is possible to verity some algorithms, but the software implementations of those algorithms are not always perfect. We can try to rely on automated proof systems, but they are also subject to having errors.

Third, there is the question of what you mean by "errors". Some important systems have fairly "fuzzy" requirement specifications. Error usually means "not conforming to the specification", but the specification itself, being created (most cases) by a human, is subject to both error and incompleteness. Humans aren't very good at thinking about "everything".

Fourth, things change. A correctly operating software system exists in a changing world. Processors change, operating systems change, associated software (libraries) change. So it is difficult to say whether a system that was working properly last year continues to do so. Even when all the parts are "correct", the interactions may introduce subtle errors.

So, some things can be done and it is useful to extend what can be done, but we are, at the moment anyway, only really able to attack the most important issues and questions. The core problems we see. Formal verification of core processes helps, but, again, algorithms and implementations are not, precisely, the same thing.

One may hope that sophisticated AI systems might help with this. But (IMO) currently available systems are flawed and overhyped. They can and do produce poor (even evil) outcomes. There is a joke in AI circles that "true" AI is ten years away and has been (to my knowledge) for at least five decades. And so it remains.

Things that can be perfectly specified can likely be proven correct. But software isn't really like that. The problem remains hard. Testing is required, but it is also imperfect. Some practices (pair programming, test first, small increments) reduce the number of errors but can't guarantee their absence.


If you want to learn an important technique in building error free software, I recommend a book: The Science of Programing by David Gries. The idea is to develop programs from pre and post conditions (specifications, actually) and program invariants.

$\endgroup$
9
  • $\begingroup$ pre and post conditions I have never read book but are you aware of Hoare logic? $\endgroup$
    – Guy Coder
    Dec 5, 2021 at 8:28
  • $\begingroup$ @GuyCoder, yes, of course. The Gries book is based on it, and on the work of Dijkstra. $\endgroup$
    – Buffy
    Dec 5, 2021 at 11:47
  • $\begingroup$ I was surprised that you did not note that in your answer. The book is expensive, unless you buy it used. the Wikipedia page while dense, is free. $\endgroup$
    – Guy Coder
    Dec 5, 2021 at 13:21
  • $\begingroup$ @GuyCoder, the book is incredibly rich in exercises for learning. There is more to learning than reading text. $\endgroup$
    – Buffy
    Dec 5, 2021 at 13:27
  • 1
    $\begingroup$ @Guy Coder had a good but brief answer. $\endgroup$ Dec 12, 2021 at 16:09
0
$\begingroup$

Is it possible to prove software to be bugless?

Within reason, e.g. Halting Problem

The most complete work I know of at present is

Verified Software Toolchain

The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context.

$\endgroup$
3
  • $\begingroup$ But, is writing an internally consistent set of assertions that completely describes the correct behavior of a software system under all possible conditions any easier than writing the code that behaves correctly under all possible conditions? (If you've ever written code in strict accordance with the rules of Test Driven Development, then you'll know why I am smiling.) $\endgroup$ Dec 8, 2021 at 4:00
  • $\begingroup$ P.S., About that Halting Problem: If I give you a supposedly consistent and complete set of assertions that describe a "halt tester" function, and you deliver code that fails to give the correct answer in finite time for certain inputs, Is that a bug? and which one of us shall we blame for it? $\endgroup$ Dec 8, 2021 at 4:05
  • $\begingroup$ @GuyCoder I rolled back the vandalism to the post, though I left it deleted. If you have a special reason to remove this beyond deletion, you can reply to me here or find me in chat. $\endgroup$
    – Ben I.
    Dec 13, 2021 at 3:36
0
$\begingroup$

There are of course some way to make proof of your algorithm, that basically by doing some mathematical demonstration.

That can be and is done in some very critical fields for instance in medical or air space but in general the cost of doing algorithm proof is way above the cost of the failure risk.

Then as Buffy said, there's also the fact that in most non-critical software you will have some dependencies that you can't afford to prove.

Testing is always about finding a compromise between cost/quality and needs. In general in industry we can not afford to prove every thing that's why the common practice is to test as much as possible. Even if some times that actually means not testing.

So yes you can definitively prove that some code is bug-less but this is very costly and the complexity is exponential regarding the size of the software and its dependencies. Regarding calculus, things can also get very complicated very fast, think about floats and filters for instance, proving that the size of the smallest float uncertainty has or hasn't an impact on your algorithm is very complex and hence very costly, and pragmatically much of the time you do not need to worry about that.

As I said it's always a risk reward kind of thing, what is the level of quality that you need, and how much are you ready to spend on that?

As Buffy also said part of the problem is that you would also end up depending on hardware that can be trusted in general but can also have flaws.

It's always a question of who/what do you trust, because you can go very deep in the rabbit hole and not even being really sure that there won't be any bug.

$\endgroup$
0
$\begingroup$

All the above answers are taking your question literally: if you have a program, how do you prove it to be correct. That is the wrong question. You should ask:

How do I make a program that is provably correct

Let me quote the famous Edsger W. Dijkstra, from his Turing Award lecture:

Today a usual technique is to make a program and then to test it. But: program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence. (cue laughter)

The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness. But one should not first make the program and then prove its correctness, because then the requirement of providing the proof would only increase the poor programmer’s burden. On the contrary: the programmer should let correctness proof and program grow hand in hand.

And now you need to read some pretty stiff literature by Dijkstra and Hoare...

An important aspect of it is proving loops correct, which you do by stating the "invariant": the predicate that is correct at the start/end of each iteration. Then the correctness of the whole loop is a result of a sort of inductive proof. In fact, if you do this the right way, the code becomes a sort of by-product of the mathematical correctness proof. And is therefore provably correct.

$\endgroup$
-1
$\begingroup$

Sort answer no: see Buffy's answer for an elaboration.

Longer answer: We can do a lot better than we currently do. Here are a few techniques.

  • Choice of language
  • Functional / no-mutation (where possible)
  • Eliminate null
  • Design by contract: pre- / post-conditions, and invariants
  • Static analysis
  • Test first
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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