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.
"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.
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
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.
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.
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.
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