Coq
Dan Tobias (Talk | contribs) |
Dan Tobias (Talk | contribs) |
||
| Line 7: | Line 7: | ||
Coq treats theorems and proofs as data types which can be manipulated by algorithms, so you can use proofs A and B as inputs into algorithm C to produce yet another, more complex, proof D, whose correctness is contingent on the validity of A and B. | Coq treats theorems and proofs as data types which can be manipulated by algorithms, so you can use proofs A and B as inputs into algorithm C to produce yet another, more complex, proof D, whose correctness is contingent on the validity of A and B. | ||
| − | Interestingly, unlike almost all other programming languages, Coq is not Turing-complete; its rules guarantee that all programs will terminate (no infinite loops are possible), which limits the range of algorithms in a similar manner to the BlooP language described by Douglas Hofstadter in his [[BlooP, FlooP, and GlooP]] group of languages to illustrate the range of computability. | + | Interestingly, unlike almost all other programming languages, Coq is not Turing-complete; its rules guarantee that all programs will terminate (no infinite loops are possible), which limits the range of algorithms in a similar manner to the BlooP language described by Douglas Hofstadter in his [[BlooP, FlooP, and GlooP]] group of languages (in his book, ''Gödel, Escher, Bach: An Eternal Golden Braid'') to illustrate the range of computability. |
== Links == | == Links == | ||
Latest revision as of 04:01, 2 May 2014
Coq is a formal language for expressing mathematical theorems and proofs as well as algorithms, intended to be used in the process of formally proving the correctness of computer programs. Formal correctness proofs of programs have existed as an academic concept for decades, usually taught in computer science curricula, but have usually been regarded as impractical for the "real world". However, the increasing computing power available now makes it more feasible to develop systems to generate such proofs in an automated manner, and there is some highly critical code (e.g., the SSL code which developed the infamous "Heartbleed" bug) that is of great importance to the technical infrastructure of the world and could benefit from a rigorous proving process.
Coq treats theorems and proofs as data types which can be manipulated by algorithms, so you can use proofs A and B as inputs into algorithm C to produce yet another, more complex, proof D, whose correctness is contingent on the validity of A and B.
Interestingly, unlike almost all other programming languages, Coq is not Turing-complete; its rules guarantee that all programs will terminate (no infinite loops are possible), which limits the range of algorithms in a similar manner to the BlooP language described by Douglas Hofstadter in his BlooP, FlooP, and GlooP group of languages (in his book, Gödel, Escher, Bach: An Eternal Golden Braid) to illustrate the range of computability.
