Answers.Body: <p>Yes, in theory, but not in practice.</p>
  <p>The problem is that a &quot;proof&quot;, like a program, might be flawed.</p>
  <p>Some things, however, aren't amenable to proof if they depend on things that can't be controlled (race conditions, for example). Modern hardware is much more complex than simple models imply.</p>
  <p>Don Knuth once said of an algorithm: &quot;Beware of bugs in the above code; I have only proved it correct, not tried it.&quot;</p>
  <hr />
  <p>In theory, theory is the same as practice, but not in practice.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2023-08-01T01:13:41.263Z
Answers.Text: Depends on your view of the practice. In my view there are well-published examples of program verification, including verified compilers (eg [CompCert](https://compcert.org) and [CakeML](https://cakeml.org)) and operating system kernels such as [seL4](https://sel4.systems). The proofs are machine checked. Contrary to your claim, concurrent programs, including those containing races are amenable to verification, too.
Answers.UserDisplayName: Kai
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2023-07-31T10:02:15.150Z
Answers.LastActivityDate: 2023-07-31T10:02:15.150Z
Answers.UserDisplayName: Buffy
Body: <p>When testing software, does people prove some part of the program to work as they want like mathematicians prove their methods to be correct?</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2023-07-31T13:35:53.697Z
Comments.Text: I love this question and would love it to stay on the site, but you need to make clear in what way it is about teaching CS. Can you edit it to make this clearer? (Just use the little "Edit" link under the question.)
Comments.UserDisplayName: Ben I.
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2023-07-31T18:09:47.940Z
Comments.Text: This would contradict the halting problem. In particular [Rice theorem](https://en.wikipedia.org/wiki/Rice's_theorem)
Comments.UserDisplayName: Rushi
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2023-08-05T20:33:53.200Z
Comments.Text: @Rusi The halting problem doses not prove that you can not determine weather a program halts. It only proves that it is trivial to construct a program that can not be proven.
Comments.UserDisplayName: ctrl-alt-delor
Tags: <mathematics><unit-testing>
Title: Can one prove a part of the program to be correct rather than test it?
ThreadText: # Can one prove a part of the program to be correct rather than test it?
  
  (Asked by: username_0 on 2023-07-31)
  
  When testing software, does people prove some part of the program to work as they want like mathematicians prove their methods to be correct?
  
  **Tags:** mathematics, unit-testing
  
  > **Comments:**
  > **username_1**: I love this question and would love it to stay on the site, but you need to make clear in what way it is about teaching CS. Can you edit it to make this clearer? (Just use the little "Edit" link under the question.)  
  > **username_2**: This would contradict the halting problem. In particular [Rice theorem](https://en.wikipedia.org/wiki/Rice's_theorem)  
  > **username_3**: @Rusi The halting problem doses not prove that you can not determine weather a program halts. It only proves that it is trivial to construct a program that can not be proven.  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_4 on 2023-07-31. Score: 1
  
  Yes, in theory, but not in practice.
  
  The problem is that a "proof", like a program, might be flawed.
  
  Some things, however, aren't amenable to proof if they depend on things that can't be controlled (race conditions, for example). Modern hardware is much more complex than simple models imply.
  
  Don Knuth once said of an algorithm: "Beware of bugs in the above code; I have only proved it correct, not tried it."
  
  ---
  
  In theory, theory is the same as practice, but not in practice.
  
  > **Comments:**
  > **username_5**: Depends on your view of the practice. In my view there are well-published examples of program verification, including verified compilers (eg [CompCert](https://compcert.org) and [CakeML](https://cakeml.org)) and operating system kernels such as [seL4](https://sel4.systems). The proofs are machine checked. Contrary to your claim, concurrent programs, including those containing races are amenable to verification, too.  
  
  ---
  
  