From Newsgroup: comp.lang.c

Note: The post is so writen to post in comp.lang.c, comp.lang.c++ unmodified. 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 wrong.
The idea is that C/C++ can be a language of proofs, including logic/math.) 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
should be OK).
3. xxx are correct iff it can be implemented by Turing Machine. But normally we
don't need to go that deep because we use C/C++ language. Specification
(declaration) is fine if it can be correctly assumed correct.
4. Proof is basically valid C/C++ codes that can be compiled. Linkage is option.
(E.g. value range of type int is TBD, OK in proof)
--- Synchronet 3.21a-Linux NewsLink 1.2