<p>The powerful formalism you are looking for cannot exist, for otherwise we could solve the <a href="https://en.wikipedia.org/wiki/Halting_problem" rel="nofollow">halting problem</a>. Here is the sketch of an argument why. </p>

<p>Consider <a href="https://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow">Hoare triples</a> $\{A\} P \{B\}$ for <a href="https://en.wikipedia.org/wiki/Correctness_(computer_science)" rel="nofollow">partial correctness</a>. 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</p>

<p>$$\{\mathsf{True}\} P \{\mathsf{False}\}.$$ </p>

<p>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.</p>

<p>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.</p>

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

CC BY-SA 3.0
2014-11-18T17:30:13.587Z
In theory, this is right. But in practice (using analogy) we have file compression routines, because data we work with, including natural languages, contains redundancy, is far from random. So, while almost all files get longer, useful files get shorter.
Roman Susi
CC BY-SA 3.0
2014-11-18T17:32:07.510Z
@RomanSusi I'm not sure what you mean.
Martin Berger
CC BY-SA 3.0
2014-11-18T17:33:32.953Z
Can you name a few notable achievements, please, (outside of hardware verification methods)?
Roman Susi
CC BY-SA 3.0
2014-11-18T17:36:23.830Z
Full verification of an operating system kernel (seL4) by Klein et al, verification of an optimising compiler (compCert) by Leroy, verification of major mathematical proofs like the 4 colour theory (Gonthier) and Kepler's conjecture (Hales et al).
Martin Berger
CC BY-SA 3.0
2014-11-18T17:37:53.967Z
I mean that even if there were huge, properly modularized and annotated for machine-readability repository of proved algorithms, a large class of practical algorithms would be much easier to verify semi-automatically.
Roman Susi
CC BY-SA 3.0
2014-11-18T17:38:04.570Z
On a smaller scale since you asked about simple algorithms, Chargueraud verified half of Okasaki's book on purely functional data structures in Coq.
Martin Berger
CC BY-SA 3.0
2014-11-18T17:41:04.297Z
Sorry, I did not mean proofs of individual problems tackled by highly specialized minds. I meant achievements, which make verification practical. (meaning an average programmer can do it with some practice and tool)
Roman Susi
CC BY-SA 3.0
2014-11-18T17:48:48.640Z
Advanced typing systems (e.g. Scala's) and automatic testing tools are used by 'normal' programmers on a regular basis. As to logic and prover based methods, they are not yet ready for industrial prime-time. That will take another decade or two.
Martin Berger
CC BY-SA 3.0
2014-11-18T17:23:02.980Z
2014-11-18T18:14:31.563Z
2014-11-18T18:14:31.563Z
Martin Berger
<p>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 <a href="http://www.comp.nus.edu.sg/~hobor/Publications/2011/logicfs.pdf" rel="nofollow">http://www.comp.nus.edu.sg/~hobor/Publications/2011/logicfs.pdf</a> 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 (<a href="http://adam.chlipala.net/cpdt/" rel="nofollow">http://adam.chlipala.net/cpdt/</a>) tries to convince, that Coq is much easier, than many think.</p>

<p>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?</p>

<p>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.)</p>

<p>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. <strong>Added</strong>: 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.</p>

<p>Would be interesting to know, if I have overlooked something. </p>

<p><strong>EDIT</strong>: 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.</p>

<p>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.</p>

<p><strong>EDIT2</strong>: Some notable results from comments, thanks to commenters:</p>

<ul>
<li>Conflict-Driven Clause Learning - makes SAT powerful (year 1999)</li>
<li>Separation Logic - "local reasoning" (2002)</li>
</ul>

CC BY-SA 3.0
2014-11-18T15:45:00.303Z
This is a huge field, and your question is vague. Formal methods *are* practical! If you include type-checking, they are extremely widely used, but more advanced methods are widely used as well. Certainly formal verification is *not* "stuck in the seventies".
cody
CC BY-SA 3.0
2014-11-18T17:03:56.173Z
Ok, maybe verification software catches up with theories founded in seventies or programming languages drift towards more convenient constructs, but what great discovery happened after 1980, which had major impact in the practical verification and software, automating it? Can you name some?
Roman Susi
CC BY-SA 3.0
2014-11-18T18:35:01.957Z
One notable advance since the 80s: Separation Logic.
Dave Clarke
CC BY-SA 3.0
2014-11-18T21:10:51.637Z
1979: Nelson and Oppen describe a procedure for combining decision procedures, which is at the base of SMT solving. This is now one of the most powerful techniques for theorem proving. 1997/1999 Conflict Driven Clause Learning is proposed as a method to improve SAT solving. SAT solvers now ubiquitously use CDCL.
cody
CC BY-SA 3.0
2014-11-18T21:18:09.323Z
[Here](http://en.wikipedia.org/wiki/List_of_model_checking_tools) is a list of model-checking tools that are actively developed, and [here](http://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis) is a list of code analysis tools. I feel like you are willfully ignoring a huge body research and industrial tools...
cody
CC BY-SA 3.0
2014-11-19T04:43:00.877Z
Thanks you. While most of the listed tools are not what I meant in the question, some look promising.
Roman Susi
<program-verification>
Advances in program verification?
Roman Susi
# Advances in program verification?

(Asked by: username_0 on 2014-11-17)

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)

**Tags:** program-verification
> **Comments:**
> **username_1**: This is a huge field, and your question is vague. Formal methods *are* practical! If you include type-checking, they are extremely widely used, but more advanced methods are widely used as well. Certainly formal verification is *not* "stuck in the seventies".  
> **username_0**: Ok, maybe verification software catches up with theories founded in seventies or programming languages drift towards more convenient constructs, but what great discovery happened after 1980, which had major impact in the practical verification and software, automating it? Can you name some?  
> **username_2**: One notable advance since the 80s: Separation Logic.  
> **username_1**: 1979: Nelson and Oppen describe a procedure for combining decision procedures, which is at the base of SMT solving. This is now one of the most powerful techniques for theorem proving. 1997/1999 Conflict Driven Clause Learning is proposed as a method to improve SAT solving. SAT solvers now ubiquitously use CDCL.  
> **username_1**: [Here](http://en.wikipedia.org/wiki/List_of_model_checking_tools) is a list of model-checking tools that are actively developed, and [here](http://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis) is a list of code analysis tools. I feel like you are willfully ignoring a huge body research and industrial tools...  
> **username_0**: Thanks you. While most of the listed tools are not what I meant in the question, some look promising.  

---

## 1 answers

### Answer by username_3 on 2014-11-18. Score: 1

The powerful formalism you are looking for cannot exist, for otherwise we could solve the [halting problem](https://en.wikipedia.org/wiki/Halting_problem). Here is the sketch of an argument why.

Consider [Hoare triples](https://en.wikipedia.org/wiki/Hoare_logic) $\{A\} P \{B\}$ for [partial correctness](https://en.wikipedia.org/wiki/Correctness_(computer_science)). 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.

> **Comments:**
> **username_0**: In theory, this is right. But in practice (using analogy) we have file compression routines, because data we work with, including natural languages, contains redundancy, is far from random. So, while almost all files get longer, useful files get shorter.  
> **username_3**: @RomanSusi I'm not sure what you mean.  
> **username_0**: Can you name a few notable achievements, please, (outside of hardware verification methods)?  
> **username_3**: Full verification of an operating system kernel (seL4) by Klein et al, verification of an optimising compiler (compCert) by Leroy, verification of major mathematical proofs like the 4 colour theory (Gonthier) and Kepler's conjecture (Hales et al).  
> **username_0**: I mean that even if there were huge, properly modularized and annotated for machine-readability repository of proved algorithms, a large class of practical algorithms would be much easier to verify semi-automatically.  
> **username_3**: On a smaller scale since you asked about simple algorithms, Chargueraud verified half of Okasaki's book on purely functional data structures in Coq.  
> **username_0**: Sorry, I did not mean proofs of individual problems tackled by highly specialized minds. I meant achievements, which make verification practical. (meaning an average programmer can do it with some practice and tool)  
> **username_3**: Advanced typing systems (e.g. Scala's) and automatic testing tools are used by 'normal' programmers on a regular basis. As to logic and prover based methods, they are not yet ready for industrial prime-time. That will take another decade or two.  

---

