How to prove Halting Problem in C?
From
wij@3:633/280.2 to
All on Tue Aug 26 14:52:10 2025
Note: The post is so writen to post in comp.lang.c, comp.lang.c++ unmodifie=
d.
Purpose: Usage of C/C++ language, particularly in proving theories.
Halting Problem should be simple and does not involve too many stuff.
This question does not limit how the HP idea is expressed in C/C++. The TM = can
be expressed as a function, executable,...
(There are already many pseudo-codes in the internet)
1. The correctness of C/C++ codes is based on Turing Machine.
(Otherwise, no way to verify. Or, you porved Church-Turing thesis is wro= ng.
The idea is that C/C++ can be a language of proofs, including logic/mat= h.)
2. C++std library does not prove itself correct, the proof generally cannot
relies on it (except you can prove the part used. Some primative things=
=20
should be OK).
3. xxx are correct iff it can be implemented by Turing Machine. But normall=
y we
don't need to go that deep because we use C/C++ language. Specification=
=20
(declaration) is fine if it can be correctly assumed correct.
4. Proof is basically valid C/C++ codes that can be compiled. Linkage is op= tion.
(E.g. value range of type int is TBD, OK in proof)
--- MBSE BBS v1.1.2 (Linux-x86_64)
* Origin: A noiseless patient Spider (3:633/280.2@fidonet)