My POV here was very cautious, as I didn't exclude programs which can be proved. The problem is that even if control flow is "provable", a lot of algorithms use

My POV here was very cautious, as I didn't exclude programs which can be proved. The problem is that even if control flow is "provable", a lot of algorithms use number computations and is much harder to deal with from a formal POV : "In cooperation with the University of Iowa and Rockwell Collins, this research focuses on the verification of safety properties on Lustre pro-grams. SAT or SMT, based verification approaches such as k-induction give good results on programs with a mostly discrete state space (boolean, bounded integers). However, when numerical computations are involved (real/float computations) the formalization of the property to be proved often needs to be strengthened using auxiliary lemmas to make it inductive with respect to the system’s transition relation. When attempted manually the discovery of such lemmas is time consuming and hinders the efficiency and scalability of formal verification. Automating lemma discovery hence appears crucial to allowing end-users to apply formal verification on industrial cases." Taken from [0] The seminars I attended to, from the creators of coq (a formal verification language), didn't disagree with this point of view. Of course, formal verification is not the only thing we can do [0]. In any case, what you propose seem interesting, if the halting problem was the only problem to solve to have a formally proven system. [0] http://www.aerospacelab-journal.org/sites/www.aerospacelab-journal.org/files/AL04-10_1.pdf http://www.aerospacelab-journal.org/sites/www.aerospacelab-j...