Advances in program verification?

Question

While trying to check what is the state of art in formal verification, it seemed to me that there were actually no breakthroughs in decades. For example, here http://www.comp.nus.edu.sg/~hobor/Publications/2011/logicfs.pdf it is stated, that 5-line (imperative) factorial program needs something like 100 lines of Coq code. And I consider Coq to be one of the best tools out there! Adam Chlipala's book (http://adam.chlipala.net/cpdt/) tries to convince, that Coq is much easier, than many think.

So, the first question goes, are there any advances in the field (and what they are), which would make formal methods practical any time soon?

If no, then has any researcher explained this seeming discrepancy between the fact, that programming languages become easier to use (become higher and higher level, handle specific domains better), while formal verification methods seemingly remain in the seventies of last century? (I guess, on the functional programming front situation is a bit better, but still.)

My own speculation on this paradox is that maybe some fundamental, powerful computation formalism is yet to be discovered (that is, the problem lays with the language). Another answer could be, that the complexity gap is inherent in the mathematics, and no development of the theory could destroy it. Personally, I do not believe in the latter case, because all the history of development in mathematics. Added: Third possibility is that for some reason re-use of formal proofs and tactics, finding new axioms is difficult. In "normal" software it is possible to share libraries, which are used to build more complex structures, and these components are stacked together to form even bigger systems. "Normal" software is times easier to develop now than 30-40 years ago.

Would be interesting to know, if I have overlooked something.

EDIT: It may well be, that some narrow problem domains enjoy nice, easy-to-use verification tools, for example, languages with regular grammars may be easy to deal with. This question is not about such cases.

To narrow my question, lets consider one toy example, which is surely broadly known, and which I consider general enough kind of programming problem. Suppose, I want to implement an ADT Queue using two Stacks (another ADT). I write down a solution (it's a couple of methods: enqueue and dequeue). Now, I want a formal proof, that my solution is indeed a Queue (suppose, I have some kind of description of it's behavior). I can program it from assembler to, say, APL and get a size from 2 lines to 100. Now, how long will be the proof? I bet, it's about a page on paper. But what if I have semi-automatic tool? I guess, the proof will be (for imperative case) almost as long as assembler program, will need several insights to come with and the result is much more cryptic in case one needs to manually re-check. And of course, I am not sure how type-checking is going to help in this case.

EDIT2: Some notable results from comments, thanks to commenters:

• Conflict-Driven Clause Learning - makes SAT powerful (year 1999)
• Separation Logic - "local reasoning" (2002)

Answer 1

The powerful formalism you are looking for cannot exist, for otherwise we could solve the halting problem. Here is the sketch of an argument why.

Consider Hoare triples $\{A\} P \{B\}$ for partial correctness. If we had a (computable) upper bound that related program length to the lengths of correctness proofs, then we could apply it to the assertion

$$\{\mathsf{True}\} P \{\mathsf{False}\}.$$

This assertion is true exactly when $P$ loops. Since we have assumed a (computable) upper bound for proof length, we can find such a proof, were it to exist, in finite time by brute force search, giving an algorithms for deciding the halting problem. Contradiction. The argument can be adapted for other formal methods.

That means, regardless of the specifics, there will always be short programs with long proofs. One way to find such programs is to look at difficult or open number theoretic questions like Fermat's last theorem or the twin prime conjecture: you can write short programs that diagonialise over the natural numbers, looking for counterexamples. Proving that such programs do or do not terminate is likely to be highly involved.

All that being said, the last decade has seen an explosion of work on formal verification and a great deal of progress.