Regarding the final paragraph of Neel's answerNeel's answer 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.
replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
Regarding the final paragraph of Neel's answer 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.
Regarding the final paragraph of Neel's answer 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.
I think the answer to the first question is that generally it is too much worktoo much work with current tools. To get the ideafeeling, I suggest you try provingtrying to prove the correctness of Bubble Sort in Coq (or if you prefer a little more try proving the correctness ofchallenge, 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.
TheThis 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 for 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 who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. But in general the current tools needsneed a lot of development (including their SE and HCI aspects) to becomebefore becoming useful for general programmers (and mathematicians).
Regarding the final paragraph of Neel's answer 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(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 programsproblems 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 complete$AC^0$-complete for the complexity class, therefore it contains all the 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" if you are interested. (A draft 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 doesn'tdoes 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 a provably total program to get one which the theory cannotis 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, or we can. 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.)
I think the answer to the first question is that generally it is too much work with current tools. To get the idea I suggest you try proving the correctness of Bubble Sort in Coq (or if you prefer a little more try proving the correctness of 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.
The 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 for 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 who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. But in general the current tools needs a lot of development (including their SE and HCI aspects) to become useful for general programmers (and mathematicians).
Regarding final paragraph of Neel's answer, actually it is easy to prove even more. 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 programs 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 complete for the complexity class, therefore it contains all the 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. Cook and P. Nguyen's recent book "Logical Foundations of Proof Complexity" if you are interested. (A draft 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 doesn't 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 a provably total program to get one which the theory cannot 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 which is the more common practice, or we can try to prove the mathematical statement describing the problem using restricted means and then extract a verified program from it. (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.)
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 who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. 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 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" if you are interested. (A draft 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.)
I think the answer forto the first question is that generally it is too much work with current tools. To get the idea I suggest you try proving the correctness of Bubble Sort in Coq (or if you prefer a little more try proving the correctness of 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.
The 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 for 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 who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. But in general the current tools needs a lot of development (including their SE and HCI aspects) to become usableuseful for general programmerprogrammers (and mathematicianmathematicians).
Regarding final paragraph of Neel's answer, actually it is easy to prove even more. It is reasonable to expect that the syntax of any programing language shouldwill 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 programs 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 complete for the complexity class, therefore it contains all the 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, checksee S. Cook and P. Nguyen's recent book "Logical Foundations of Proof Complexity" if you are interested. (A draft 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 doesn't 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 a provably total program to get one which the theory cannot 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 which is the more common practice, or we can try to prove the mathematical statement describing the problem using restricted means and then extract a verified program from it. (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.)
I think the answer for the first question is that generally it is too much work with current tools. To get the idea I suggest you try proving correctness of Bubble Sort in Coq (or if you prefer a little more try 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.
The 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.
This does not mean that there has not been successful cases of verified programs. I know that there are groups who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. But in general the current tools needs a lot of development (including their SE and HCI aspects) to become usable for general programmer (and mathematician).
Regarding final paragraph of Neel's answer, actually it is easy to prove even more. It is reasonable to expect that the syntax of any programing language should 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 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 programs in the complexity class are provably total in a very weak theories. The basic idea is that the provably total functions of the theory contains all $AC^0$ functions and a problem which is complete for the complexity class. The relation between proofs and complexity theory is studied in proof complexity, check S. Cook and P. Nguyen's recent book "Logical Foundations of Proof Complexity" if you are interested. (A draft 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 doesn't 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 a provably total program to get one which the theory cannot prove its totality.
I think the answer to the first question is that generally it is too much work with current tools. To get the idea I suggest you try proving the correctness of Bubble Sort in Coq (or if you prefer a little more try proving the correctness of 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.
The 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 for 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 who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. But in general the current tools needs a lot of development (including their SE and HCI aspects) to become useful for general programmers (and mathematicians).
Regarding final paragraph of Neel's answer, actually it is easy to prove even more. 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 programs 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 complete for the complexity class, therefore it contains all the 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. Cook and P. Nguyen's recent book "Logical Foundations of Proof Complexity" if you are interested. (A draft 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 doesn't 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 a provably total program to get one which the theory cannot 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 which is the more common practice, or we can try to prove the mathematical statement describing the problem using restricted means and then extract a verified program from it. (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.)