<p>"Certifying compiler" usually means something slightly different: it means that you have a compiler which can prove that the machine code it emits correctly implements the high-level semantics. That is, this is a proof that there are no compiler bugs. The programs that people give to the compiler can still be wrong, but the compiler will generate a correct machine code version of the wrong program. The biggest success story along these lines is the <a href="http://compcert.inria.fr/" rel="noreferrer">CompCert verified compiler</a>, which is a compiler for a large subset of C. </p>

<p>The Compcert compiler itself is a program with a correctness proof (done in Coq), which guarantees that if it generates code for a program, it will be correct (with respect to the operational semantics of assembly &amp; C that the CompCert designers used).  The effort to machine-check these things is quite large; typically the correctness proof will be anywhere from 1x to 100x the size of the program you are verifying. Writing machine-checked programs and proofs is a new skill you have to learn -- it's not mathematics or programming as usual, though it depends on being able to do both well. It feels like you are starting from scratch, like being a novice programmer again. </p>

<p>There are no special theoretical barriers to this, though. The only thing along these lines is the <a href="http://dx.doi.org/10.1016/S0019-9958(67)90546-3" rel="noreferrer" title="&#39;On the Size of Machines&#39;, Blum 1967">Blum Size theorem</a> that for any language in which all programs are total, you can find a program in a general recursive language which will be at least exponentially larger when programmed in the total language. The way to understand this result is that a total language encodes not just a program, but also a termination proof. So you can have short programs with long termination proofs. However, this doesn't really matter in practice, since we're only going to ever write programs with manageable termination proofs. </p>

<p>EDIT: Dai Le asked for some elaboration of the last point. </p>

<p>This is mostly a pragmatic claim, based on the fact that if you can understand why a program works, then it's unlikely that the reason is  some vast invariant millions of pages long. (The longest invariants I've used are a few pages long, and boy do they make the reviewers grumble! Understandably so, too, since the invariant is the reason the program works stripped of all the narrative that helps people understand it.) </p>

<p>But there are also some theoretical reasons, as well. Basically, we don't know very many ways to systematically invent programs whose correctness proofs are very long. The main method is to (1) take the logic in which you prove correctness, (2) find a property which can't be directly expressed in that logic (consistency proofs are the typical source), and (3) find a program whose correctness proof relies on a family of expressible consequences of the inexpressible property. Because (2) is inexpressible, this means that the proof of each expressible consequence must be done independently, which lets you blow up the size of the correctness proof. As a simple example, note that in first-order logic with a parent relation, you can't express the ancestor relation. But $k$-ancestry (ancestry of depth $k$) is expressible, for each fixed $k$. So by giving a program that uses some property of ancestry up to some depth (say, 100), you can force a correctness proof in FOL to contain proofs of those properties a hundred times over. </p>

<p>The sophisticated take on this subject is called "reverse mathematics", and is the study of which axioms are required to prove given theorems. I don't know that much about it, but if you post a question on its application to CS, and I'm sure at least Timothy Chow, and probably several other people,  will be able to tell you interesting things.</p>

CC BY-SA 2.5
2011-01-01T22:46:26.840Z
Could you please elaborate this point "we're only going to ever write programs with manageable termination proofs" a bit more?
Dai Le
CC BY-SA 2.5
2011-01-02T19:57:00.757Z
Thanks for your updated answer! Your answer really opens my perspective. Actually I myself also works a bit on "reverse mathematics", but I didn't realize the connection you mentioned. Thanks again!
Dai Le
CC BY-SA 3.0
2016-07-01T04:53:39.347Z
The point in your edit is related to the fact that we have hardly any candidates for tautologies that require long proofs in natural proof systems (like, say, Frege). Part of the reason for this is that the only way we know a tautology is tautologous in the first place is because we had a proof in mind, which necessarily wasn't so long!
Joshua Grochow
CC BY-SA 3.0
2011-01-01T22:33:05.223Z
2015-05-25T21:05:27.357Z
2015-05-25T21:05:27.357Z
Neel Krishnaswami
<p>I think the answer to the first question is that generally it is <em>too much work</em> with current tools. To get the feeling, I suggest trying to prove the correctness of Bubble Sort in Coq (or if you prefer a little more challenge, use Quick Sort). I don't think it is reasonable to expect programmers write verified programs as long as proving correctness of such basic algorithms is so difficult and time consuming.</p>

<p>This question is similar to asking why mathematicians don't write formal proofs verifiable by proof checkers? Writing a program with a formal correctness proof means proving a mathematical theorem about the written code, and the answer to that question also applies to your question.</p>

<p>This does not mean that there has not been successful cases of verified programs. I know that there are <a href="http://www.verisoftxt.de/StartPage.html" rel="nofollow noreferrer">groups</a> who are proving the correctness of systems like <a href="http://www.microsoft.com/hyper-v-server/en/us/default.aspx" rel="nofollow noreferrer">Microsoft's hypervisor</a>. A related case is Microsoft's <a href="http://research.microsoft.com/en-us/projects/vcc/" rel="nofollow noreferrer">Verified C Compiler</a>. But in general the current tools need a lot of development (including their SE and HCI aspects) before becoming useful for general programmers (and mathematicians).</p>

<p>Regarding the final paragraph of <a href="https://cstheory.stackexchange.com/questions/4052/what-do-we-know-about-provably-correct-programs/4055#4055">Neel's answer</a> about program size growth for languages with only total functions, actually it is easy to prove even more (If I understood it correctly). It is reasonable to expect that the syntax of any programing language will be c.e. and the set of total computable functions is not c.e., so for any programming language where all programs are total there is a total computable function which cannot be computed by any program (of any size) in that language.</p>

<hr>

<p>For the second question, I answered a similar question on Scott's blog sometime ago. Basically if the complexity class has a nice characterization and is computably representable (i.e. it is c.e.) then we can prove that some representation of the problems in the complexity class are provably total in a very weak theories corresponding to the complexity class. The basic idea is that the provably total functions of the theory contains all $AC^0$ functions and a problem which is $AC^0$-complete for the complexity class, therefore it contains all problems in the complexity class and can prove the totality of those programs. The relation between proofs and complexity theory is studied in proof complexity, see S.A. Cook and P. Nguyen's recent book "<a href="http://www.cup.es/us/catalogue/catalogue.asp?isbn=9780521517294" rel="nofollow noreferrer">Logical Foundations of Proof Complexity</a>" if you are interested. (A <a href="http://www.cs.toronto.edu/~sacook/homepage/book" rel="nofollow noreferrer">draft</a> from 2008 is available.) So the basic answer is that for many classes "Provably C = C". </p>

<p>This is not true in general since there are semantic complexity classes which do not have syntactic characterization, e.g. total computable functions. If by recursive you mean total recursive functions then the two are not equal, and the set of computable functions which are provably total in a theory is well studied in proof theory literature and are called <em>the provably total functions</em> of the theory. For example: the provably total functions of $PA$ are $\epsilon_0$-recursive functions (or equivalently functions in Godel's system $T$), the provably total functions of $PA^2$ are function in Girard's system $F$, the provably total functions of $I\Sigma_1$ are primitive recursive functions, ... . </p>

<p>But it does not seem to me that this means much in program verification context, since there are also programs which are extensionally computing the same function but we cannot prove that the two programs are computing the same function, i.e. the programs are extensionally equal but not intentionally. (This is similar to the Morning Star and the Evening Star.) Moreover it is easy to modify a given provably total program to get one which the theory is unable to prove its totality.</p>

<hr>

<p>I think the two questions are related. The objective is to get a verified program. A verified programs means that the program satisfies a description, which is a mathematical statement. One way is to write a program in a programming language and then prove its properties like it satisfies the description, which is the more common practice. Another option is to try to prove the mathematical statement describing the problem using restricted means and then extract a verified program from it. For example, if we prove in the theory corresponding to $P$ that for any given number $n$ there is a sequence of prime numbers which their product is equal to $n$, then we can extract a $P$ algorithm for factorization from the proof. (There are also researcher who try to automatize the first approach as much as possible, but checking interesting non-trivial properties of programs is computationally difficult and cannot be completely verified without false positives and negatives.)</p>

CC BY-SA 2.5
2011-01-02T21:53:54.633Z
Nice answer! You mention that one way is to extract programs from proofs, which is something one can do automatically in Coq, for example. A related area is *proof mining*, where people (working usually in mathematical logic) try to extract information from a given proof. For example, it's possible in some cases to (automatically) find an intuitionistic proof given a classical one.
Radu GRIGore
CC BY-SA 2.5
2011-01-02T22:10:25.483Z
@Radu: thanks for pointing out that it can be done automatically in Coq. As you mentioned one can also extract some constructive information and therefore programs from classical proofs of theorem using proof mining for some classes of formulas (interested people can check [Ulrich Kuhlenbach](http://www.mathematik.tu-darmstadt.de/~kohlenbach/)'s papers for details). Another possibly related result is that if a $\Pi^0_2$ theorem is proven in $PA$, it is also provable constructively in $HA$ by Harvey Friedman's translation.
_
Kaveh
CC BY-SA 2.5
2011-01-03T06:27:06.743Z
Andrej Bauer has a new interesting post on his blog in which he proves [Godel's Dialectica Interpretation in Coq](http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/).
Kaveh
CC BY-SA 2.5
2011-01-02T19:20:28.443Z
2011-01-02T22:33:44.067Z
2017-04-13T12:32:30.623Z
Kaveh
<p>What you are asking about in the first question is sometimes called a "verifying compiler", and a few years ago Tony Hoare offered it as <a href="http://cs-www.cs.yale.edu/homes/dachuan/Grand/HoareCC.pdf">a grand challenge for computing research</a>.  To some extent this already exists and is in active use in tools such as the <a href="http://coq.inria.fr/">Coq theorem prover</a>, which organize the problem by way of <a href="http://en.wikipedia.org/wiki/Type_theory">type theory</a> and the propositions-as-types principle ("<a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard</a>").</p>

<p>EDIT: just wanted to add emphasis on "to some extent".  This is far from a solved problem, but the success of Coq gives hope that it is not a pipe dream.</p>

CC BY-SA 2.5
2011-01-03T17:04:07.133Z
I would say that building verified software is where building plain old software was in 1956. It was already obvious that software was going to be incredibly important, and there were already major success stories. However, people were still many missing fundamental concepts (a clear understanding of what procedures and variables were, for example), and the distance from theory to practice could be as short as implementing Lisp by programming up the code in a theorem. This is an INCREDIBLY exciting time to be working on languages and verification.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-02T12:36:08.833Z
2011-01-03T16:41:04.600Z
2011-01-03T16:41:04.600Z
Noam Zeilberger
<p>A tool that checks whether a program is correct is sometimes called a program verifier. In this context, "correct" usually means two things: that the program never produces certain outputs (think segmentation fault, NullPointerException, etc.) and that the program agrees with a specification.</p>

<p>The code and the specification may agree and still be perceived as wrong. In a sense, asking developers to write specifications is like asking two developers to solve the problem. If the two implementations agree then you have higher confidence that they are OK. In another sense, however, specifications are better than a second implementation. Because the specification needs not be efficient or even executable, it can be much more succinct and hence harder to get wrong.</p>

<p>With these caveats in mind, I recommend you look at the <a href="http://research.microsoft.com/en-us/projects/specsharp/">Spec# program verifier</a>.</p>

CC BY-SA 2.5
2011-01-02T13:39:33.410Z
As far as I understand Spec# (and its extension Sing#), it gives the programmer the ability to statically verify asserts, but it does not require the programmer does this, nor does it provide the ability to prove arbitrary properties of the code.
Alex ten Brink
CC BY-SA 2.5
2011-01-02T16:11:40.820Z
Arbitrary properties can be encoded as fol assertions, in principle. I'm not sure what you want the tool to require. Do you want the specs to say what the output should be for all possible inputs?
Radu GRIGore
CC BY-SA 2.5
2011-01-02T09:45:25.790Z
2011-01-02T09:45:25.790Z
Radu GRIGore
<p><a href="https://doi.org/10.1137/1.9781611970395.ch6" rel="nofollow noreferrer">Chapter 6</a> of the following classic monograph studies almost exactly your second question:</p>
<blockquote>
<p>Hartmanis, J. <a href="http://www.ams.org/mathscinet-getitem?mr=506684" rel="nofollow noreferrer">Feasible computations and provable complexity properties</a>, CBMS-NSF Regional Conference Series in Applied Mathematics, 30. Society for Industrial and Applied Mathematics (SIAM), Philadelphia, Pa., 1978.</p>
</blockquote>
<p>For example, he defines the class &quot;F-TIME[T(n)]&quot; (where F is some reasonable formal proof system) to be <span class="math-container">$\{L(M_i) | T_i(n) \leq T(n) \text{ is provable in F}\}$</span> (where <span class="math-container">$M_i$</span> is the i-th Turing machine in a complete list of TMs, and <span class="math-container">$T_i(n)$</span> is the maximum running time of <span class="math-container">$M_i$</span> on inputs of length <span class="math-container">$n$</span>). Let me just highlight a few results relevant to your question - many more can be found in the monograph and references therein:</p>
<blockquote>
<p>Cor. 6.4: Let <span class="math-container">$T(n) \geq n \log(n)$</span> be a computable function, and let <span class="math-container">$g(n) \geq 1$</span> be an unbounded computable function. Then <span class="math-container">$F$</span>-<span class="math-container">$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$</span>.</p>
</blockquote>
<blockquote>
<p>Theorem 6.5: There exist computable monotonically increasing time bounds <span class="math-container">$T(n)$</span> for which <span class="math-container">$F$</span>-<span class="math-container">$TIME[T(n)] \neq TIME[T(n)]$</span>.</p>
</blockquote>
<blockquote>
<p>Theorem 6.14: For any computable
<span class="math-container">$T(n) \geq n \log(n)$</span>, <span class="math-container">$TIME[T(n)] = \{
L(M_i) | \text{F proves} (\exists j)[L(M_j) = L(M_i) \wedge T_j(n) \leq T(n)]
\}$</span>.</p>
</blockquote>
<p>For space, however, the situation is better controlled:</p>
<blockquote>
<p>Theorem 6.9:
(1) If <span class="math-container">$s(n) \geq n$</span> is space-constructible, then <span class="math-container">$SPACE[s(n)] = F$</span>-<span class="math-container">$SPACE[s(n)]$</span>.</p>
</blockquote>
<blockquote>
<p>(2) If <span class="math-container">$SPACE[S(n)]=F$</span>-<span class="math-container">$SPACE[S(n)]$</span> (<span class="math-container">$S(n) \geq n$</span>) then there is a space-constructible <span class="math-container">$s(n)$</span> such that <span class="math-container">$SPACE[S(n)]=SPACE[s(n)]$</span>.</p>
</blockquote>

CC BY-SA 4.0
2016-07-01T06:24:46.610Z
2020-12-24T06:18:21.063Z
2020-12-24T06:18:21.063Z
Joshua Grochow
<p>In the general case, it is impossible to create an algorithm that confirms whether an algorithm is equivalent to a specification. This is an informal proof:</p>

<p>Almost all programming languages are Turing-complete. Therefore, any language decided by a TM can be also be decided by a program written in this language.</p>

<p>The problem of determining whether two TMs accept the same language, known as $Equivalence/TM$ is undecidable. As a consequence of Turing completeness, the same holds for the programs of the given language. In other words, it is undecidable to know whether the inputs you want your program to accept and the inputs it really does are the same.</p>

<p>Furthermore, $Equivalence/TM$ is not even recursive enumerable. That is because $Non-emptiness/TM$ (whether a TM accepts at least one input) is an acceptable language, since you can iterate over all possible inputs. If the TM is non-empty, eventually you will find a word that is accepted. Therefore $Emptiness/TM$ is unacceptable, otherwise $Emptiness/TM$ would be decidable (which we know it is not). However Emptiness/TM can be reduced to $Equivalence/TM$, therefore $Equivalence/TM$ is also unacceptable. Therefore you can use an algorithm whether or not two machines are not equivalent, but you cannot be sure if they are equivalent, or you haven't given your algorithm enough time.</p>

<p>However, this is only for the general case. It is possible that you can decide whether or not the specifications are equivalent to the program, by solving a more relaxed version of the problem. For example, you might examine only a number of inputs or say that the two programs are equivalent with some uncertainty. This is what software testing is all about.</p>

<p>As for the rest of your questions:</p>

<p>Note: This part has been edited for clarification. It turns out that I did the mistake I was trying to avoid, sorry.</p>

<p>Let $TrueR$ be the collection of languages that we know to be decidable. Of course $TrueR \subseteq R$. One can then prove the following:</p>

<p>$ProvableR = TrueR$. It is easy to see that $ProvableR \subset TrueR$. However, it is also $TrueR \subset ProvableR$ . The proof is very easy: Let $A  \epsilon TrueR$ . By definition , in every input $A$ returns either YES or NO. Therefore, $A$ halts on every input. It follows that $A \epsilon ProvableR$ .</p>

<p>Informally , this can be summarized as: You don't know that a language is decidable until you have proven it to be. So if in a formal system you have the knowledge that a language is decidable, this knowledge can also serve as a proof for that. Therefore, you cannot simultaneously have the knowledge that a language is both decidable and it cannot be proven so, these two statements are mutually exclusive. </p>

<p>My final point is that our knowledge is partial and that the only way of studying $R$ is through $ProvableR$. The distinction might make sense in mathematics and we can acknowledge it, but we possess no tools to study it. Since $ProvableR \subset R$ , we are bound to never completely know $R$ in its entirety.</p>

<p>@Kaveh summarizes it best: Provable always means provable in some system/theory and does not coincide with truth in general. </p>

<p>The same holds for any other complexity class: To determine membership you need a proof first. This is why I believe that your second question is too general, since it contains not only complexity theory, but also computation theory as well, depending on the property you want the language to have.</p>

CC BY-SA 2.5
2011-01-02T18:52:47.373Z
That bit about $R\subset ProvableR$ seems a bit fishy. Why must there be a proof for a language to be decidable? Actually, it seems there is not (in general): determining whether a TM's halting set is a recursive language is $\Sigma^0_3$ complete. If there were a proof that a TM's halting set was Recursive, it would be in $\Sigma^0_1$.
Mark Reitblatt
CC BY-SA 2.5
2011-01-02T19:49:03.967Z
Provable always means provable in some system/theory and does not coincide with truth in general.
Kaveh
CC BY-SA 2.5
2011-01-02T20:13:27.840Z
I see now that for my question to be interesting, one should talk about the set of halting Turing machines, not the set of decidable languages.
Alex ten Brink
CC BY-SA 2.5
2011-01-02T20:25:35.963Z
@Alex Well, you need some way of talking about languages, but there's uncountably many. So, if you want to talk about languages connected to some finite object (like a proof), you need to restrict yourself to languages identifiable by a finite object, like a TM.
Mark Reitblatt
CC BY-SA 2.5
2011-01-03T12:19:43.800Z
I am not saying that for every decidable language there is a proof that it is decidable. I am saying that if you know that a proof exists (you don't even have to know the proof) that a machine always halts, then by definition this language is decidable. I will edit the answer to clarify this.
chazisop
CC BY-SA 2.5
2011-01-03T17:52:54.157Z
@chazisop That doesn't seem to make sense. Are you saying that we "know" every provably decidable language? I'm not even sure what that means; why should the definition of a formal class make mention of personal knowledge?
Mark Reitblatt
CC BY-SA 2.5
2011-01-04T00:36:05.137Z
If you know that a language is provably decidable (even if you don't know the proof but only its existence), then you know it is decidable. Although a formal class has a certain definition, our understanding of it can be limited and depend on our knowledge , as a whole and not personally.
chazisop
CC BY-SA 2.5
2011-01-04T09:09:10.773Z
chazisop, as I said, provable means provable in a (fixed) theory, and for every reasonable theory (c.e., consistent, ...) there is some total computable function which cannot be proven to be total in that theory. There are total functions which cannot be proven to be total in ZFC (and reasonable extensions of it). You are confusing the notion of truth with provability. So the proof does not work (assuming that $R$ means total recursive).
Kaveh
CC BY-SA 2.5
2011-01-04T09:15:45.077Z
ps: I think it would be clear if you used $True$ in place of $Know$ (unless you are an [intuitionist](http://en.wikipedia.org/wiki/Intuitionism), see also [the intuitionism article on SEP](http://plato.stanford.edu/entries/intuitionism/)).
Kaveh
CC BY-SA 2.5
2011-01-04T13:19:48.603Z
Kaveh I agree with you. I am just pointing out that our only tool is proofs, which do not suffice to know the complete truth. In your example, all that I am saying is that although we know that they are non-provable total computable functions, we cannot study them (we only know that they exist).  As for the $R$ proof, my second edit meant to clarify that my approach to $ProvableR = R$ was wrong. Your comment settles that $ ProvableR \subset R$
chazisop
CC BY-SA 2.5
2011-01-05T00:15:54.487Z
Your answer still says $ProvableR=TrueR$, which I think is not correct. Here are four notions: 1. those computable functions that we know (*right now*) that are total, 2. those that can proven to be total in a (fixed reasonable) theory (like ZFC), 3. those that we *in principle* can know that they are total, and 4. those that are total. You are still talking about knowing a result which is not very usual in classical mathematics. And $ProvableR \subseteq R$ is not clear, e.g. if the theory is not *sound* then it can prove some functions are total while they are not really total.
Kaveh
CC BY-SA 2.5
2011-01-05T00:16:11.880Z
Your argument: "... it is also $TrueR\subseteq ProvableR$. ... Let $AϵTrueR$. By definition , [o]n every input $A$ returns either YES or NO. Therefore, $A$ halts on every input. It follows that $AϵProvableR$." is incorrect, the last step does not work. The function halts on every input (this statement is true) but that does not mean that this fact can be proven in $ZFC$.
Kaveh
CC BY-SA 2.5
2011-01-05T02:20:20.353Z
Let me state it differently, your argument shows: $\vdash (A \in R \rightarrow A \in R)$ which is obvious, what you need to show is: $\vdash (A \in R \rightarrow "ZFC \vdash A \in R")$, which cannot be proven.
Kaveh
CC BY-SA 2.5
2011-01-05T16:10:19.500Z
Yes, I think I can see what you meant earlier. I have a question however : In category 3 , what do you mean by in principle: That the language seems to be decidable but we do not have a full proof yet (like we do for Church-Turing thesis) or that we believe that the language is decidable but we do not have strong evidence (like for P vs NP)?
chazisop
CC BY-SA 2.5
2011-01-02T18:35:30.010Z
2011-01-04T13:23:25.277Z
2011-01-04T13:23:25.277Z
chazisop
<p>The question has to be posed correctly. For example, nobody ever wants to know whether an actual program would complete given infinite memory and some means of accessing it (maybe an operation to move the base address by some number). Turing's theorem is irrelevant to program correctness in any concrete sense and people who cite it as a barrier to program verification are confusing two quite different things. When engineers/programmers talk of program correctness they want to know about finite properties. This is also pretty much true for mathematicians who are interested in whether something is provable. Godel's letter <a href="http://vyodaiken.com/2009/08/28/godels-lost-letter/" rel="nofollow">http://vyodaiken.com/2009/08/28/godels-lost-letter/</a> explains this in some detail. </p>

<blockquote>
  <p>Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine. After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem. </p>
</blockquote>

<p>It may well be infeasible to examine the immense state set of a program executing on an actual computer and detect bad states, there is no theoretical reason why it can't be done. In fact, there has been a lot of progress in this field - for example see <a href="http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf" rel="nofollow">http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf</a> (thanks to Neil Immerman for telling me about this) </p>

<p>A different and more difficult problem is specifying exactly what properties one wants a program to have in order to be correct. </p>

CC BY-SA 3.0
2015-05-27T02:50:33.800Z
2015-05-27T02:56:37.087Z
2015-05-27T02:56:37.087Z
Victor Yodaiken
<p>The ever increasing complexity of computer programs and the increasingly crucial position computers have in our society leaves me wondering why we still don't collectively use programming languages in which you have to give a formal proof that your code works correctly.</p>

<p>I believe the term is a 'certifying compiler' (I found it <a href="https://cstheory.stackexchange.com/questions/2815/what-do-we-know-about-restricted-versions-of-the-halting-problem/2816#2816">here</a>): a compiler compiling a programming language in which one not only has to write the code, but also state the specification of the code and prove that the code adheres to the specification (or use an automated prover to do so).</p>

<p>While searching the internet, I only found projects that either use a very simple programming language or failed projects that try to adapt modern programming languages. This leads me to my question:</p>

<blockquote>
  <p>Are there any certifying compilers implementing a full-blown programming language, or is this very hard/theoretically impossible?</p>
</blockquote>

<p>Additionally, I've yet to see any complexity class involving provable programs, such as 'the class of all languages decidable by a Turing machine for which a proof exists that this Turing machine halts', which I shall call <span class="math-container">$ProvableR$</span>, as an analogue to <span class="math-container">$R$</span>, the set of recursive languages.</p>

<p>I can see advantages of studying such a complexity class: for instance, for <span class="math-container">$ProvableR$</span> the Halting problem is decidable (I even conjecture <span class="math-container">$ProvableRE$</span> defined in the obvious way would be the largest class of languages for which it is decidable). In addition, I doubt we would rule out any practically useful programs: who would use a program when you can't prove it terminates?</p>

<p>So my second question is:</p>

<blockquote>
  <p>What do we know about complexity classes which require their containing languages to provably have certain properties?</p>
</blockquote>

CC BY-SA 3.0
2015-05-26T07:10:07.250Z
"Provably" is misused here several times but it's not your fault. Computer scientists do it all the time. You do not mean "provably correct programs" but presumably "programs whose correctness has been proved".
Andrej Bauer
CC BY-SA 3.0
2016-12-10T15:47:06.023Z
For the majority of programs that I spend my time working on, a proof that the program ever *does* halt would indicate a bug in the program. Many programs (for instance, the program that runs a pacemaker or a web server) should not halt in the typical case.
David Stone
CC BY-SA 2.5
2011-01-01T16:57:34.860Z
I realise I asked two questions that are essentially in two different fields in CS. Since they are closely related, I decide to go with a single question, but I could of course split them up if the powers that be think that is a better idea.
Alex ten Brink
CC BY-SA 2.5
2011-01-01T18:17:24.827Z
A compiler could enumerate all possible proofs of length i, letting i go from 1 to infinity, until it finds a proof that the program halts. If we require that the input for the compiler provably halts, then the compiler will always find that proof. Since the halting problem is undecidable, we must conclude there are programs that halt, but no proof for this exists. The crucial point is that programs are unable to find out if a proof exists, not that they are unable to find a proof if it exists.
Alex ten Brink
CC BY-SA 2.5
2011-01-01T21:39:35.190Z
I think you should split them up. They are different questions with different answers.
Mark Reitblatt
CC BY-SA 2.5
2011-01-02T11:56:44.263Z
On the first question, an influential paper is "Social processes and proofs of theorems and programs", http://portal.acm.org/citation.cfm?id=359106
Colin McQuillan
CC BY-SA 2.5
2011-01-02T16:24:23.913Z
Program verification is undecidable. So one problem is to say what constitutes a good solution. See http://cstheory.stackexchange.com/questions/4016/is-there-a-sensible-notion-of-an-approximation-algorithm-for-an-undecidable-probl
Radu GRIGore
CC BY-SA 2.5
2011-01-02T16:48:00.700Z
@Colin, I read the paper you linked. While it was an interesting read and posed a number of valid points, I was surprised by the adversarial tone of the paper.
Alex ten Brink
CC BY-SA 2.5
2011-01-02T18:23:04.390Z
@Colin: that paper is worth reading for its analysis of proof, but its predictions have been falsified. Today we have provably correct compilers, operating system kernels, garbage collectors, and databases, all of which they predicted to be impossible. The trick to evade their critique was to avoid human verification of the low-level details of formal proofs, but to use machine verification of proofs, and use humans to verify the proof checker. Noam's ref to type theory is where the state of the art is, which leaves imperative programs in something of a bind since type theory is functional.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-04T16:54:25.087Z
@Alex: if a program halts on a given input, then its execution trace is a proof that it halts.
Hence, if a program halts, then given enough time a computer can always prove it.
However, there exist programs that do not halt, and it can't be proved that that they don't halt.
Antonio Valerio Miceli-Barone
CC BY-SA 2.5
2011-01-05T01:37:31.233Z
@user1749: I used to believe that as well, but watch out what your reasoning proves: it proves that if a program halts *on a certain input*, you can prove this. However, since interesting languages are infinite, you can't prove always prove halting this way.
Alex ten Brink
<reference-request><complexity-classes><computability><pl.programming-languages>
What do we know about provably correct programs?
Alex ten Brink
# What do we know about provably correct programs?

(Asked by: username_0 on 2011-01-01)

The ever increasing complexity of computer programs and the increasingly crucial position computers have in our society leaves me wondering why we still don't collectively use programming languages in which you have to give a formal proof that your code works correctly.

I believe the term is a 'certifying compiler' (I found it [here](https://cstheory.stackexchange.com/questions/2815/what-do-we-know-about-restricted-versions-of-the-halting-problem/2816#2816)): a compiler compiling a programming language in which one not only has to write the code, but also state the specification of the code and prove that the code adheres to the specification (or use an automated prover to do so).

While searching the internet, I only found projects that either use a very simple programming language or failed projects that try to adapt modern programming languages. This leads me to my question:

> Are there any certifying compilers implementing a full-blown programming language, or is this very hard/theoretically impossible?

Additionally, I've yet to see any complexity class involving provable programs, such as 'the class of all languages decidable by a Turing machine for which a proof exists that this Turing machine halts', which I shall call $ProvableR$, as an analogue to $R$, the set of recursive languages.

I can see advantages of studying such a complexity class: for instance, for $ProvableR$ the Halting problem is decidable (I even conjecture $ProvableRE$ defined in the obvious way would be the largest class of languages for which it is decidable). In addition, I doubt we would rule out any practically useful programs: who would use a program when you can't prove it terminates?

So my second question is:

> What do we know about complexity classes which require their containing languages to provably have certain properties?

**Tags:** reference-request, complexity-classes, computability, pl.programming-languages
> **Comments:**
> **username_0**: I realise I asked two questions that are essentially in two different fields in CS. Since they are closely related, I decide to go with a single question, but I could of course split them up if the powers that be think that is a better idea.  
> **username_0**: A compiler could enumerate all possible proofs of length i, letting i go from 1 to infinity, until it finds a proof that the program halts. If we require that the input for the compiler provably halts, then the compiler will always find that proof. Since the halting problem is undecidable, we must conclude there are programs that halt, but no proof for this exists. The crucial point is that programs are unable to find out if a proof exists, not that they are unable to find a proof if it exists.  
> **username_3**: I think you should split them up. They are different questions with different answers.  
> **username_4**: On the first question, an influential paper is "Social processes and proofs of theorems and programs", http://portal.acm.org/citation.cfm?id=359106  
> **username_5**: Program verification is undecidable. So one problem is to say what constitutes a good solution. See http://cstheory.stackexchange.com/questions/4016/is-there-a-sensible-notion-of-an-approximation-algorithm-for-an-undecidable-probl  
> **username_0**: @Colin, I read the paper you linked. While it was an interesting read and posed a number of valid points, I was surprised by the adversarial tone of the paper.  
> **username_6**: @Colin: that paper is worth reading for its analysis of proof, but its predictions have been falsified. Today we have provably correct compilers, operating system kernels, garbage collectors, and databases, all of which they predicted to be impossible. The trick to evade their critique was to avoid human verification of the low-level details of formal proofs, but to use machine verification of proofs, and use humans to verify the proof checker. Noam's ref to type theory is where the state of the art is, which leaves imperative programs in something of a bind since type theory is functional.  
> **username_7**: @Alex: if a program halts on a given input, then its execution trace is a proof that it halts. Hence, if a program halts, then given enough time a computer can always prove it. However, there exist programs that do not halt, and it can't be proved that that they don't halt.  
> **username_0**: @user1749: I used to believe that as well, but watch out what your reasoning proves: it proves that if a program halts *on a certain input*, you can prove this. However, since interesting languages are infinite, you can't prove always prove halting this way.  
> **username_1**: "Provably" is misused here several times but it's not your fault. Computer scientists do it all the time. You do not mean "provably correct programs" but presumably "programs whose correctness has been proved".  
> **username_2**: For the majority of programs that I spend my time working on, a proof that the program ever *does* halt would indicate a bug in the program. Many programs (for instance, the program that runs a pacemaker or a web server) should not halt in the typical case.  

---

## 7 answers

### Answer by username_6 on 2011-01-01. Score: 29

"Certifying compiler" usually means something slightly different: it means that you have a compiler which can prove that the machine code it emits correctly implements the high-level semantics. That is, this is a proof that there are no compiler bugs. The programs that people give to the compiler can still be wrong, but the compiler will generate a correct machine code version of the wrong program. The biggest success story along these lines is the [CompCert verified compiler](http://compcert.inria.fr/), which is a compiler for a large subset of C.

The Compcert compiler itself is a program with a correctness proof (done in Coq), which guarantees that if it generates code for a program, it will be correct (with respect to the operational semantics of assembly & C that the CompCert designers used). The effort to machine-check these things is quite large; typically the correctness proof will be anywhere from 1x to 100x the size of the program you are verifying. Writing machine-checked programs and proofs is a new skill you have to learn -- it's not mathematics or programming as usual, though it depends on being able to do both well. It feels like you are starting from scratch, like being a novice programmer again.

There are no special theoretical barriers to this, though. The only thing along these lines is the [Blum Size theorem](http://dx.doi.org/10.1016/S0019-9958(67)90546-3 "'On the Size of Machines', Blum 1967") that for any language in which all programs are total, you can find a program in a general recursive language which will be at least exponentially larger when programmed in the total language. The way to understand this result is that a total language encodes not just a program, but also a termination proof. So you can have short programs with long termination proofs. However, this doesn't really matter in practice, since we're only going to ever write programs with manageable termination proofs.

EDIT: Dai Le asked for some elaboration of the last point.

This is mostly a pragmatic claim, based on the fact that if you can understand why a program works, then it's unlikely that the reason is some vast invariant millions of pages long. (The longest invariants I've used are a few pages long, and boy do they make the reviewers grumble! Understandably so, too, since the invariant is the reason the program works stripped of all the narrative that helps people understand it.)

But there are also some theoretical reasons, as well. Basically, we don't know very many ways to systematically invent programs whose correctness proofs are very long. The main method is to (1) take the logic in which you prove correctness, (2) find a property which can't be directly expressed in that logic (consistency proofs are the typical source), and (3) find a program whose correctness proof relies on a family of expressible consequences of the inexpressible property. Because (2) is inexpressible, this means that the proof of each expressible consequence must be done independently, which lets you blow up the size of the correctness proof. As a simple example, note that in first-order logic with a parent relation, you can't express the ancestor relation. But $k$-ancestry (ancestry of depth $k$) is expressible, for each fixed $k$. So by giving a program that uses some property of ancestry up to some depth (say, 100), you can force a correctness proof in FOL to contain proofs of those properties a hundred times over.

The sophisticated take on this subject is called "reverse mathematics", and is the study of which axioms are required to prove given theorems. I don't know that much about it, but if you post a question on its application to CS, and I'm sure at least Timothy Chow, and probably several other people, will be able to tell you interesting things.

> **Comments:**
> **username_8**: Could you please elaborate this point "we're only going to ever write programs with manageable termination proofs" a bit more?  
> **username_8**: Thanks for your updated answer! Your answer really opens my perspective. Actually I myself also works a bit on "reverse mathematics", but I didn't realize the connection you mentioned. Thanks again!  
> **username_9**: The point in your edit is related to the fact that we have hardly any candidates for tautologies that require long proofs in natural proof systems (like, say, Frege). Part of the reason for this is that the only way we know a tautology is tautologous in the first place is because we had a proof in mind, which necessarily wasn't so long!  

---

### Answer by username_10 on 2011-01-02. Score: 23

I think the answer to the first question is that generally it is *too much work* with current tools. To get the feeling, I suggest trying to prove the correctness of Bubble Sort in Coq (or if you prefer a little more challenge, use Quick Sort). I don't think it is reasonable to expect programmers write verified programs as long as proving correctness of such basic algorithms is so difficult and time consuming.

This question is similar to asking why mathematicians don't write formal proofs verifiable by proof checkers? Writing a program with a formal correctness proof means proving a mathematical theorem about the written code, and the answer to that question also applies to your question.

This does not mean that there has not been successful cases of verified programs. I know that there are [groups](http://www.verisoftxt.de/StartPage.html) who are proving the correctness of systems like [Microsoft's hypervisor](http://www.microsoft.com/hyper-v-server/en/us/default.aspx). A related case is Microsoft's [Verified C Compiler](http://research.microsoft.com/en-us/projects/vcc/). But in general the current tools need a lot of development (including their SE and HCI aspects) before becoming useful for general programmers (and mathematicians).

Regarding the final paragraph of [Neel's answer](https://cstheory.stackexchange.com/questions/4052/what-do-we-know-about-provably-correct-programs/4055#4055) about program size growth for languages with only total functions, actually it is easy to prove even more (If I understood it correctly). It is reasonable to expect that the syntax of any programing language will be c.e. and the set of total computable functions is not c.e., so for any programming language where all programs are total there is a total computable function which cannot be computed by any program (of any size) in that language.

---

For the second question, I answered a similar question on Scott's blog sometime ago. Basically if the complexity class has a nice characterization and is computably representable (i.e. it is c.e.) then we can prove that some representation of the problems in the complexity class are provably total in a very weak theories corresponding to the complexity class. The basic idea is that the provably total functions of the theory contains all $AC^0$ functions and a problem which is $AC^0$-complete for the complexity class, therefore it contains all problems in the complexity class and can prove the totality of those programs. The relation between proofs and complexity theory is studied in proof complexity, see S.A. Cook and P. Nguyen's recent book "[Logical Foundations of Proof Complexity](http://www.cup.es/us/catalogue/catalogue.asp?isbn=9780521517294)" if you are interested. (A [draft](http://www.cs.toronto.edu/~sacook/homepage/book) from 2008 is available.) So the basic answer is that for many classes "Provably C = C".

This is not true in general since there are semantic complexity classes which do not have syntactic characterization, e.g. total computable functions. If by recursive you mean total recursive functions then the two are not equal, and the set of computable functions which are provably total in a theory is well studied in proof theory literature and are called *the provably total functions* of the theory. For example: the provably total functions of $PA$ are $\epsilon\_0$-recursive functions (or equivalently functions in Godel's system $T$), the provably total functions of $PA^2$ are function in Girard's system $F$, the provably total functions of $I\Sigma\_1$ are primitive recursive functions, ... .

But it does not seem to me that this means much in program verification context, since there are also programs which are extensionally computing the same function but we cannot prove that the two programs are computing the same function, i.e. the programs are extensionally equal but not intentionally. (This is similar to the Morning Star and the Evening Star.) Moreover it is easy to modify a given provably total program to get one which the theory is unable to prove its totality.

---

I think the two questions are related. The objective is to get a verified program. A verified programs means that the program satisfies a description, which is a mathematical statement. One way is to write a program in a programming language and then prove its properties like it satisfies the description, which is the more common practice. Another option is to try to prove the mathematical statement describing the problem using restricted means and then extract a verified program from it. For example, if we prove in the theory corresponding to $P$ that for any given number $n$ there is a sequence of prime numbers which their product is equal to $n$, then we can extract a $P$ algorithm for factorization from the proof. (There are also researcher who try to automatize the first approach as much as possible, but checking interesting non-trivial properties of programs is computationally difficult and cannot be completely verified without false positives and negatives.)

> **Comments:**
> **username_5**: Nice answer! You mention that one way is to extract programs from proofs, which is something one can do automatically in Coq, for example. A related area is *proof mining*, where people (working usually in mathematical logic) try to extract information from a given proof. For example, it's possible in some cases to (automatically) find an intuitionistic proof given a classical one.  
> **username_10**: @Radu: thanks for pointing out that it can be done automatically in Coq. As you mentioned one can also extract some constructive information and therefore programs from classical proofs of theorem using proof mining for some classes of formulas (interested people can check [Ulrich Kuhlenbach](http://www.mathematik.tu-darmstadt.de/~kohlenbach/)'s papers for details). Another possibly related result is that if a $\Pi^0_2$ theorem is proven in $PA$, it is also provable constructively in $HA$ by Harvey Friedman's translation. _  
> **username_10**: Andrej Bauer has a new interesting post on his blog in which he proves [Godel's Dialectica Interpretation in Coq](http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/).  

---

### Answer by username_11 on 2011-01-02. Score: 18

What you are asking about in the first question is sometimes called a "verifying compiler", and a few years ago Tony Hoare offered it as [a grand challenge for computing research](http://cs-www.cs.yale.edu/homes/dachuan/Grand/HoareCC.pdf). To some extent this already exists and is in active use in tools such as the [Coq theorem prover](http://coq.inria.fr/), which organize the problem by way of [type theory](http://en.wikipedia.org/wiki/Type_theory) and the propositions-as-types principle ("[Curry-Howard](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)").

EDIT: just wanted to add emphasis on "to some extent". This is far from a solved problem, but the success of Coq gives hope that it is not a pipe dream.

> **Comments:**
> **username_6**: I would say that building verified software is where building plain old software was in 1956. It was already obvious that software was going to be incredibly important, and there were already major success stories. However, people were still many missing fundamental concepts (a clear understanding of what procedures and variables were, for example), and the distance from theory to practice could be as short as implementing Lisp by programming up the code in a theorem. This is an INCREDIBLY exciting time to be working on languages and verification.  

---

### Answer by username_5 on 2011-01-02. Score: 12

A tool that checks whether a program is correct is sometimes called a program verifier. In this context, "correct" usually means two things: that the program never produces certain outputs (think segmentation fault, NullPointerException, etc.) and that the program agrees with a specification.

The code and the specification may agree and still be perceived as wrong. In a sense, asking developers to write specifications is like asking two developers to solve the problem. If the two implementations agree then you have higher confidence that they are OK. In another sense, however, specifications are better than a second implementation. Because the specification needs not be efficient or even executable, it can be much more succinct and hence harder to get wrong.

With these caveats in mind, I recommend you look at the [Spec# program verifier](http://research.microsoft.com/en-us/projects/specsharp/).

> **Comments:**
> **username_0**: As far as I understand Spec# (and its extension Sing#), it gives the programmer the ability to statically verify asserts, but it does not require the programmer does this, nor does it provide the ability to prove arbitrary properties of the code.  
> **username_5**: Arbitrary properties can be encoded as fol assertions, in principle. I'm not sure what you want the tool to require. Do you want the specs to say what the output should be for all possible inputs?  

---

### Answer by username_9 on 2016-07-01. Score: 5

[Chapter 6](https://doi.org/10.1137/1.9781611970395.ch6) of the following classic monograph studies almost exactly your second question:

> Hartmanis, J. [Feasible computations and provable complexity properties](http://www.ams.org/mathscinet-getitem?mr=506684), CBMS-NSF Regional Conference Series in Applied Mathematics, 30. Society for Industrial and Applied Mathematics (SIAM), Philadelphia, Pa., 1978.

For example, he defines the class "F-TIME[T(n)]" (where F is some reasonable formal proof system) to be $\{L(M\_i) | T\_i(n) \leq T(n) \text{ is provable in F}\}$ (where $M\_i$ is the i-th Turing machine in a complete list of TMs, and $T\_i(n)$ is the maximum running time of $M\_i$ on inputs of length $n$). Let me just highlight a few results relevant to your question - many more can be found in the monograph and references therein:

> Cor. 6.4: Let $T(n) \geq n \log(n)$ be a computable function, and let $g(n) \geq 1$ be an unbounded computable function. Then $F$-$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$.

> Theorem 6.5: There exist computable monotonically increasing time bounds $T(n)$ for which $F$-$TIME[T(n)] \neq TIME[T(n)]$.

> Theorem 6.14: For any computable
> $T(n) \geq n \log(n)$, $TIME[T(n)] = \{
> L(M\_i) | \text{F proves} (\exists j)[L(M\_j) = L(M\_i) \wedge T\_j(n) \leq T(n)]
> \}$.

For space, however, the situation is better controlled:

> Theorem 6.9:
> (1) If $s(n) \geq n$ is space-constructible, then $SPACE[s(n)] = F$-$SPACE[s(n)]$.

> (2) If $SPACE[S(n)]=F$-$SPACE[S(n)]$ ($S(n) \geq n$) then there is a space-constructible $s(n)$ such that $SPACE[S(n)]=SPACE[s(n)]$.


---

### Answer by username_12 on 2011-01-02. Score: 4

In the general case, it is impossible to create an algorithm that confirms whether an algorithm is equivalent to a specification. This is an informal proof:

Almost all programming languages are Turing-complete. Therefore, any language decided by a TM can be also be decided by a program written in this language.

The problem of determining whether two TMs accept the same language, known as $Equivalence/TM$ is undecidable. As a consequence of Turing completeness, the same holds for the programs of the given language. In other words, it is undecidable to know whether the inputs you want your program to accept and the inputs it really does are the same.

Furthermore, $Equivalence/TM$ is not even recursive enumerable. That is because $Non-emptiness/TM$ (whether a TM accepts at least one input) is an acceptable language, since you can iterate over all possible inputs. If the TM is non-empty, eventually you will find a word that is accepted. Therefore $Emptiness/TM$ is unacceptable, otherwise $Emptiness/TM$ would be decidable (which we know it is not). However Emptiness/TM can be reduced to $Equivalence/TM$, therefore $Equivalence/TM$ is also unacceptable. Therefore you can use an algorithm whether or not two machines are not equivalent, but you cannot be sure if they are equivalent, or you haven't given your algorithm enough time.

However, this is only for the general case. It is possible that you can decide whether or not the specifications are equivalent to the program, by solving a more relaxed version of the problem. For example, you might examine only a number of inputs or say that the two programs are equivalent with some uncertainty. This is what software testing is all about.

As for the rest of your questions:

Note: This part has been edited for clarification. It turns out that I did the mistake I was trying to avoid, sorry.

Let $TrueR$ be the collection of languages that we know to be decidable. Of course $TrueR \subseteq R$. One can then prove the following:

$ProvableR = TrueR$. It is easy to see that $ProvableR \subset TrueR$. However, it is also $TrueR \subset ProvableR$ . The proof is very easy: Let $A \epsilon TrueR$ . By definition , in every input $A$ returns either YES or NO. Therefore, $A$ halts on every input. It follows that $A \epsilon ProvableR$ .

Informally , this can be summarized as: You don't know that a language is decidable until you have proven it to be. So if in a formal system you have the knowledge that a language is decidable, this knowledge can also serve as a proof for that. Therefore, you cannot simultaneously have the knowledge that a language is both decidable and it cannot be proven so, these two statements are mutually exclusive.

My final point is that our knowledge is partial and that the only way of studying $R$ is through $ProvableR$. The distinction might make sense in mathematics and we can acknowledge it, but we possess no tools to study it. Since $ProvableR \subset R$ , we are bound to never completely know $R$ in its entirety.

@Kaveh summarizes it best: Provable always means provable in some system/theory and does not coincide with truth in general.

The same holds for any other complexity class: To determine membership you need a proof first. This is why I believe that your second question is too general, since it contains not only complexity theory, but also computation theory as well, depending on the property you want the language to have.

> **Comments:**
> **username_3**: That bit about $R\subset ProvableR$ seems a bit fishy. Why must there be a proof for a language to be decidable? Actually, it seems there is not (in general): determining whether a TM's halting set is a recursive language is $\Sigma^0_3$ complete. If there were a proof that a TM's halting set was Recursive, it would be in $\Sigma^0_1$.  
> **username_10**: Provable always means provable in some system/theory and does not coincide with truth in general.  
> **username_0**: I see now that for my question to be interesting, one should talk about the set of halting Turing machines, not the set of decidable languages.  
> **username_3**: @Alex Well, you need some way of talking about languages, but there's uncountably many. So, if you want to talk about languages connected to some finite object (like a proof), you need to restrict yourself to languages identifiable by a finite object, like a TM.  
> **username_12**: I am not saying that for every decidable language there is a proof that it is decidable. I am saying that if you know that a proof exists (you don't even have to know the proof) that a machine always halts, then by definition this language is decidable. I will edit the answer to clarify this.  
> **username_3**: @chazisop That doesn't seem to make sense. Are you saying that we "know" every provably decidable language? I'm not even sure what that means; why should the definition of a formal class make mention of personal knowledge?  
> **username_12**: If you know that a language is provably decidable (even if you don't know the proof but only its existence), then you know it is decidable. Although a formal class has a certain definition, our understanding of it can be limited and depend on our knowledge , as a whole and not personally.  
> **username_10**: chazisop, as I said, provable means provable in a (fixed) theory, and for every reasonable theory (c.e., consistent, ...) there is some total computable function which cannot be proven to be total in that theory. There are total functions which cannot be proven to be total in ZFC (and reasonable extensions of it). You are confusing the notion of truth with provability. So the proof does not work (assuming that $R$ means total recursive).  
> **username_10**: ps: I think it would be clear if you used $True$ in place of $Know$ (unless you are an [intuitionist](http://en.wikipedia.org/wiki/Intuitionism), see also [the intuitionism article on SEP](http://plato.stanford.edu/entries/intuitionism/)).  
> **username_12**: Kaveh I agree with you. I am just pointing out that our only tool is proofs, which do not suffice to know the complete truth. In your example, all that I am saying is that although we know that they are non-provable total computable functions, we cannot study them (we only know that they exist).  As for the $R$ proof, my second edit meant to clarify that my approach to $ProvableR = R$ was wrong. Your comment settles that $ ProvableR \subset R$  
> **username_10**: Your answer still says $ProvableR=TrueR$, which I think is not correct. Here are four notions: 1. those computable functions that we know (*right now*) that are total, 2. those that can proven to be total in a (fixed reasonable) theory (like ZFC), 3. those that we *in principle* can know that they are total, and 4. those that are total. You are still talking about knowing a result which is not very usual in classical mathematics. And $ProvableR \subseteq R$ is not clear, e.g. if the theory is not *sound* then it can prove some functions are total while they are not really total.  
> **username_10**: Your argument: "... it is also $TrueR\subseteq ProvableR$. ... Let $AϵTrueR$. By definition , [o]n every input $A$ returns either YES or NO. Therefore, $A$ halts on every input. It follows that $AϵProvableR$." is incorrect, the last step does not work. The function halts on every input (this statement is true) but that does not mean that this fact can be proven in $ZFC$.  
> **username_10**: Let me state it differently, your argument shows: $\vdash (A \in R \rightarrow A \in R)$ which is obvious, what you need to show is: $\vdash (A \in R \rightarrow "ZFC \vdash A \in R")$, which cannot be proven.  
> **username_12**: Yes, I think I can see what you meant earlier. I have a question however : In category 3 , what do you mean by in principle: That the language seems to be decidable but we do not have a full proof yet (like we do for Church-Turing thesis) or that we believe that the language is decidable but we do not have strong evidence (like for P vs NP)?  

---

### Answer by username_13 on 2015-05-27. Score: 1

The question has to be posed correctly. For example, nobody ever wants to know whether an actual program would complete given infinite memory and some means of accessing it (maybe an operation to move the base address by some number). Turing's theorem is irrelevant to program correctness in any concrete sense and people who cite it as a barrier to program verification are confusing two quite different things. When engineers/programmers talk of program correctness they want to know about finite properties. This is also pretty much true for mathematicians who are interested in whether something is provable. Godel's letter <http://vyodaiken.com/2009/08/28/godels-lost-letter/> explains this in some detail.

> Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine. After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem.

It may well be infeasible to examine the immense state set of a program executing on an actual computer and detect bad states, there is no theoretical reason why it can't be done. In fact, there has been a lot of progress in this field - for example see <http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf> (thanks to Neil Immerman for telling me about this)

A different and more difficult problem is specifying exactly what properties one wants a program to have in order to be correct.


---

