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

CC BY-SA 4.0
2023-08-01T01:13:41.263Z
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.
Kai
CC BY-SA 4.0
2023-07-31T10:02:15.150Z
2023-07-31T10:02:15.150Z
Buffy
<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>

CC BY-SA 4.0
2023-07-31T13:35:53.697Z
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.)
Ben I.
CC BY-SA 4.0
2023-07-31T18:09:47.940Z
This would contradict the halting problem. In particular [Rice theorem](https://en.wikipedia.org/wiki/Rice's_theorem)
Rushi
CC BY-SA 4.0
2023-08-05T20:33:53.200Z
@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.
ctrl-alt-delor
<mathematics><unit-testing>
Can one prove a part of the program to be correct rather than test it?
# 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.  

---

