3
$\begingroup$

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)
$\endgroup$
  • 3
    $\begingroup$ 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". $\endgroup$ – cody Nov 18 '14 at 15:45
  • $\begingroup$ 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? $\endgroup$ – Roman Susi Nov 18 '14 at 17:03
  • 1
    $\begingroup$ One notable advance since the 80s: Separation Logic. $\endgroup$ – Dave Clarke Nov 18 '14 at 18:35
  • 1
    $\begingroup$ 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. $\endgroup$ – cody Nov 18 '14 at 21:10
  • 1
    $\begingroup$ Here is a list of model-checking tools that are actively developed, and here is a list of code analysis tools. I feel like you are willfully ignoring a huge body research and industrial tools... $\endgroup$ – cody Nov 18 '14 at 21:18
1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Roman Susi Nov 18 '14 at 17:30
  • $\begingroup$ @RomanSusi I'm not sure what you mean. $\endgroup$ – Martin Berger Nov 18 '14 at 17:32
  • $\begingroup$ Can you name a few notable achievements, please, (outside of hardware verification methods)? $\endgroup$ – Roman Susi Nov 18 '14 at 17:33
  • 1
    $\begingroup$ 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). $\endgroup$ – Martin Berger Nov 18 '14 at 17:36
  • $\begingroup$ 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. $\endgroup$ – Roman Susi Nov 18 '14 at 17:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.