What do we know about provably correct programs? 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): 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?
"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, 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 &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. 

There are no special theoretical barriers to this, though. The only thing along these lines is the Blum Size theorem 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.