Answers.Body: <p>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:</p>
  <blockquote>
  <p>How do I make a program that is provably correct</p>
  </blockquote>
  <p>Let me quote the famous Edsger W. Dijkstra, from his Turing Award lecture:</p>
  <blockquote>
  <p>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)</p>
  </blockquote>
  <blockquote>
  <p>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.</p>
  </blockquote>
  <p>And now you need to read some pretty stiff literature by Dijkstra and Hoare...</p>
  <p>An important aspect of it is proving loops correct, which you do by stating the &quot;invariant&quot;: 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.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-24T16:13:11.630Z
Answers.LastActivityDate: 2021-12-24T16:13:11.630Z
Answers.UserDisplayName: Victor Eijkhout
Answers.Body: <blockquote>
  <p>Is it possible to prove software to be bugless?</p>
  </blockquote>
  <p>Within reason, e.g. <a href="https://en.wikipedia.org/wiki/Halting_problem" rel="nofollow noreferrer">Halting Problem</a></p>
  <p>The most complete work I know of at present is</p>
  <p><a href="https://vst.cs.princeton.edu/" rel="nofollow noreferrer">Verified Software Toolchain</a></p>
  <blockquote>
  <p>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.</p>
  </blockquote>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-08T04:00:40.170Z
Answers.Text: 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.)
Answers.UserDisplayName: Solomon Slow
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-08T04:05:59.327Z
Answers.Text: 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?
Answers.UserDisplayName: Solomon Slow
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-13T03:36:37.367Z
Answers.Text: @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.
Answers.UserDisplayName: Ben I.
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-04T14:54:18.330Z
Answers.LastActivityDate: 2021-12-13T03:34:19.063Z
Answers.LastEditDate: 2021-12-13T03:34:19.063Z
Answers.UserDisplayName: Guy Coder
Answers.Body: <p>There are of course some way to make proof of your algorithm, that basically by doing some mathematical demonstration.</p>
  <p>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.</p>
  <p>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.</p>
  <p>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.</p>
  <p>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.</p>
  <p>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?</p>
  <p>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.</p>
  <p>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.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-23T14:33:54.790Z
Answers.LastActivityDate: 2021-12-23T14:33:54.790Z
Answers.UserDisplayName: YCN-
Answers.Body: <p>Sort answer no: see Buffy's answer for an elaboration.</p>
  <p>Longer answer: We can do a lot better than we currently do.
  Here are a few techniques.</p>
  <ul>
  <li>Choice of language</li>
  <li>Functional / no-mutation (where possible)</li>
  <li>Eliminate null</li>
  <li>Design by contract: pre- / post-conditions, and invariants</li>
  <li>Static analysis</li>
  <li>Test first</li>
  </ul>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-12T16:06:06.173Z
Answers.LastActivityDate: 2021-12-12T16:06:06.173Z
Answers.UserDisplayName: ctrl-alt-delor
Answers.Body: <p>&quot;In theory, theory is the same as practice, but not in practice.&quot; (Often attributed to Yogi Berra).</p>
  <p>Let me try to explain why the problem is hard - harder than it seems. Some things can be formally verified, others not.</p>
  <p>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.</p>
  <p>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.</p>
  <p>Third, there is the question of what you mean by &quot;errors&quot;. Some important systems have fairly &quot;fuzzy&quot; requirement specifications. Error usually means &quot;not conforming to the specification&quot;, 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 &quot;everything&quot;.</p>
  <p>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 &quot;correct&quot;, the interactions may introduce subtle errors.</p>
  <p>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.</p>
  <p>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 &quot;true&quot; AI is ten years away and has been (to my knowledge) for at least five decades. And so it remains.</p>
  <p>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.</p>
  <hr />
  <p>If you want to learn an important technique in building error free software, I recommend a book: <a href="https://rads.stackoverflow.com/amzn/click/com/038790641X" rel="nofollow noreferrer" rel="nofollow noreferrer">The Science of Programing</a> by David Gries. The idea is to develop programs from pre and post conditions (specifications, actually) and program invariants.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-05T08:28:35.953Z
Answers.Text: `pre and post conditions` I have never read book but are you aware of [Hoare logic](https://en.wikipedia.org/wiki/Hoare_logic)?
Answers.UserDisplayName: Guy Coder
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-05T11:47:52.130Z
Answers.Text: @GuyCoder, yes, of course. The Gries book is based on it, and on the work of Dijkstra.
Answers.UserDisplayName: Buffy
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-05T13:21:07.783Z
Answers.Text: 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.
Answers.UserDisplayName: Guy Coder
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-05T13:27:21.183Z
Answers.Text: @GuyCoder, the book is incredibly rich in exercises for learning. There is more to learning than reading text.
Answers.UserDisplayName: Buffy
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-12T16:09:01.377Z
Answers.Text: @Guy Coder had a good but brief answer.
Answers.UserDisplayName: ctrl-alt-delor
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-12T16:11:21.923Z
Answers.Text: Note that a proof that it is possible to write a program that can not be reasoned about (the halting problem). Does not prove that it is impossible to write a program that can be reasoned about: We need to stop making excuses, and start writing better quality programs. I do not claim that we can eliminate all bugs, but we can eliminate 90% of them.
Answers.UserDisplayName: ctrl-alt-delor
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-12T16:15:11.920Z
Answers.Text: @ctrl-alt-delor, yes, good individual and team practice can prevent those pesky bugs from flying unwanted into our programs. But 90% is far too low a standard.
Answers.UserDisplayName: Buffy
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-13T19:58:56.780Z
Answers.Text: https://xkcd.com/844/
Answers.UserDisplayName: Buffy
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-17T18:14:42.587Z
Answers.Text: @Buffy. Yes, we can do a lot better, but if I were to say that, then I would not be believed.
Answers.UserDisplayName: ctrl-alt-delor
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-12-04T14:54:55.427Z
Answers.LastActivityDate: 2021-12-04T17:07:48.500Z
Answers.LastEditDate: 2021-12-04T17:07:48.500Z
Answers.UserDisplayName: Buffy
Body: <p>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.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2021-12-04T11:04:48.083Z
Comments.Text: 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.
Comments.UserDisplayName: njuffa
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2021-12-04T11:23:10.960Z
Comments.Text: 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](https://doi.org/10.1098/rsta.2015.0399))
Comments.UserDisplayName: njuffa
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2021-12-04T11:40:42.910Z
Comments.Text: "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).
Comments.UserDisplayName: Erwan
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2021-12-16T05:09:44.780Z
Comments.Text: First formally define the definition of a bug
Comments.UserDisplayName: Shmuel Newmark
Tags: <mathematics><debugging>
Title: Is it possible to prove software to be bugless?
ThreadText: # Is it possible to prove software to be bugless?
  
  (Asked by: username_0 on 2021-12-04)
  
  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.
  
  **Tags:** mathematics, debugging
  
  > **Comments:**
  > **username_1**: 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.  
  > **username_1**: 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](https://doi.org/10.1098/rsta.2015.0399))  
  > **username_2**: "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).  
  > **username_3**: First formally define the definition of a bug  
  
  ---
  
  ## 5 answers
  
  ### Answer by username_10 on 2021-12-04. Score: 2 | Accepted answer
  
  "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](https://rads.stackoverflow.com/amzn/click/com/038790641X) by David Gries. The idea is to develop programs from pre and post conditions (specifications, actually) and program invariants.
  
  > **Comments:**
  > **username_5**: `pre and post conditions` I have never read book but are you aware of [Hoare logic](https://en.wikipedia.org/wiki/Hoare_logic)?  
  > **username_10**: @username_5, yes, of course. The Gries book is based on it, and on the work of Dijkstra.  
  > **username_5**: 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.  
  > **username_10**: @username_5, the book is incredibly rich in exercises for learning. There is more to learning than reading text.  
  > **username_9**: @username_5 had a good but brief answer.  
  > **username_9**: Note that a proof that it is possible to write a program that can not be reasoned about (the halting problem). Does not prove that it is impossible to write a program that can be reasoned about: We need to stop making excuses, and start writing better quality programs. I do not claim that we can eliminate all bugs, but we can eliminate 90% of them.  
  > **username_10**: @username_9, yes, good individual and team practice can prevent those pesky bugs from flying unwanted into our programs. But 90% is far too low a standard.  
  > **username_10**: https://xkcd.com/844/  
  > **username_9**: @username_10. Yes, we can do a lot better, but if I were to say that, then I would not be believed.  
  
  ---
  
  ### Answer by username_4 on 2021-12-24. Score: 0
  
  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.
  
  
  ---
  
  ### Answer by username_5 on 2021-12-04. Score: 0
  
  > Is it possible to prove software to be bugless?
  
  Within reason, e.g. [Halting Problem](https://en.wikipedia.org/wiki/Halting_problem)
  
  The most complete work I know of at present is
  
  [Verified Software Toolchain](https://vst.cs.princeton.edu/)
  
  > 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.
  
  > **Comments:**
  > **username_6**: 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.)  
  > **username_6**: 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?  
  > **username_7**: @username_5 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.  
  
  ---
  
  ### Answer by username_8 on 2021-12-23. Score: 0
  
  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 username_10 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 username_10 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.
  
  
  ---
  
  ### Answer by username_9 on 2021-12-12. Score: -1
  
  Sort answer no: see username_10'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
  
  
  ---
  
  