14

All but the most trivial programs are filled with bugs and so anything that promises to remove them is extremely alluring. At the moment, correctness proofs are code are extremely esoteric, mainly because of the difficultly of learning this and the extra effort it takes to prove a program correct. Do you think that code proving will ever take off?

Improve this question

10 Answers 10

Reset to default
8

Not really in that sense, but pure functional programming is good in this domain. If you use Haskell, it's likely that your program is correct if the code compiles. Except from IO, a good type system is a good help.

Also programming to contract can be helpful. See Microsoft Code Contracts

Improve this answer
2
  • 6
    Sorry - I've not done much "real world" Haskell, but I've done enough tutorial exercises for several lifetimes. Just because it compiles doesn't mean it's that likely to work. Compared with e.g. Ada (chosen because it's a strictly statically typed imperative language), I'd say Haskell is a bit easier, but mostly because it's more concise (lower cyclomatic complexity). When dealing with the IO monad, there are annoyances that can make Haskell more difficult to get right - it's just different enough from imperative style that there are things it can't do as naturally.
    – user8709
    Dec 22, 2011 at 16:24
  • On "can't do as naturally", consider a "while" loop. Yes, you can roll your own - but the while condition must be within the monad because it needs react to side-effects of the loop body. Not only does this mean you've been given permission to cause side-effects within the while condition, it also makes it awkward to use that while loop. End result - it's generally easier to use recursion even in IO monad code - and that means you have to structure things in a particular way.
    – user8709
    Dec 22, 2011 at 16:28
14

All but the most trivial programs

cannot be fully proofed to be correct with reasonable effort. For any formal proof of correctness, you need at least a formal spec, and that spec has to be complete and correct. This is typically nothing you can easily create for most real-world programs. For example, try to write such a spec for something like the user interface of this discussion site, and you know what I mean.

Here I found a nice article on the topic:

http://www.encyclopedia.com/doc/1O11-programcorrectnessproof.html

Improve this answer
3
  • Right - for any programming project there's a transition from an informal description of the problem to a formal one (typically, today, in the form of a program), and that isn't going away.
    – David Thornley
    Dec 22, 2011 at 15:22
  • astree.ens.fr See Industrial Applications of Astrée here
    – zw324
    Feb 11, 2012 at 1:29
  • @ZiyaoWei: such tools are helpful, but they find only some formal errors, not more. If a one-line program like printf("1") is correct or not (for example, because the requirement was "print a equally distributed random number from 1 to 6") cannot be decided by such a static analyser.
    – Doc Brown
    May 28, 2013 at 6:32
10

The problem with formal proofs is that it only moves the problem back a step.

Saying that a program is correct is equivalent to saying that a program does what it should do. How do you define what the program should do? You specify it. And how do you define what the program should do in edge cases that the spec doesn't cover? Well, then you have to make the spec more detailed.

So let's say your spec finally becomes detailed enough to describe the correct behavior of every aspect of the entire program. Now you need a way to make your proof tools understand it. So you have to translate the spec into some sort of formal language that the proof tool can understand... hey, wait a minute!

Improve this answer
1
  • 2
    Also.. "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth
    – Brendan
    Feb 11, 2012 at 5:54
8

Formal verification has come a long way, but usually industry/widely used tools lag behind the latest research. Here's some recent efforts in this direction:

Spec# http://research.microsoft.com/en-us/projects/specsharp/ This is an extension of C# which supports code contracts (pre/post conditions and invariants) and can use these contracts to do various types of static analysis.

Similar projects to this exist for other languages, such as JML for java, and Eiffel has this pretty much built-in.

Going even further, projects like slam and blast can be used to verify certain behavioral properties with minimal programmer annotation/intervention, but still cannot deal with the full generality of modern languages (things like integer overflow/pointer arithmetic are not modeled).

I believe that we'll see much more of these techniques used in practice in the future. The main barrier is that program invariants are difficult to infer without manual annotations, and programmers are usually unwilling to provide these annotations because doing so is too tedious/time consuming.

Improve this answer
4

Not unless a method of automatically proving the code without extensive developer work arises.

Improve this answer
2
  • Consider the economic argument: maybe it's better for developers to "waste" time with correctness proofs than losing money because of software errors.
    – Andres F.
    Feb 11, 2012 at 1:54
  • I agree with fishtoaster, unless it becomes a lot less resource intensive a great deal of regular business software is just not going to have the cost/benefit to support that level of correctness. In a LOB app to a captive audience sometimes the most business benefit for cost regarding a bug report is adding a line to the docs that says "don't do that"
    – Bill
    Jun 22, 2012 at 20:34
3

Some formal methods tools (like e.g. Frama-C for critical embedded C software) can be viewed as (sort-of) providing, or at least checking, a (correctness) proof of a given software. (Frama-C check that a program obey to its formalized specification, in some sense, and respect explicitly annotated invariants in the program).

In some sectors, such formal methods are possible, e.g. as DO-178C for critical software in civilian aircraft. So in some cases, such approaches are possible and helpful.

Of course, developing less buggy software is very costly. But the formal method approach makes sense for some kind of software. If you are pessimistic, you might think that the bug are moved from the code to its formal specification (which may have some "bugs", because formalizing the intended behavior of a software is difficult and error prone).

Improve this answer
3

I stumbled on this question, and I think that this link might be interesting:

Industrial Applications of Astrée

Proving the absence of RTE in a system used by Airbus with more than 130K lines of code in 2003 does not seem to be bad, and I wonder will there be anybody say that this is not real world.

Improve this answer
2

No. The common proverb for this is, "In theory, theory and practice are the same. In practice, not."

One very simple example: Typos.

Actually running the code through unit testing finds such things almost immediately, and a cohesive set of tests will negate the need for any formal proofs. All the use cases - good, bad, error, and edge cases - should be enumerated in the unit tests, which end up as better proof the code is correct than any such proof that is separate from the code.

Especially if requirements change, or the algorithm is updated to fix a bug - the formal proof is more likely to end up out of date, same as code comments often get.

Improve this answer
12
  • 3
    Wrong. No unit tests will ever be able to cover the whole range of possible parameters. Imagine "unit testing" a compiler this way, making sure that no pass change semantics.
    – SK-logic
    Dec 22, 2011 at 16:17
  • 3
    unit testing is not the holy grail...
    – Ryathal
    Dec 22, 2011 at 16:45
  • 1
    @Winston Ewert, there are verified compilers (and many more verified assemblers). And hardware is formally verified much more often then the software. See here: gallium.inria.fr/~xleroy/publi/compiler-certif.pdf
    – SK-logic
    Dec 23, 2011 at 8:38
  • 1
    @SK-logic, yes there are toy compilers proven correct for academic purposes. But what about compilers people actually use? I suspect most compilers are checked using various forms of automated testing and almost no formal correct proofs are done.
    – Winston Ewert
    Dec 24, 2011 at 4:36
  • 1
    @Winston Ewert, correctness proofs are practical and used widely in the real life. What is not very practical is most of the modern mainstream languages. I hope they'll all die out, so the value of correctness proofs will increase in the future.
    – SK-logic
    Dec 25, 2011 at 15:19
1

I think that the limits imposed on correctness proofs because of the halting problem might be the biggest barrier to correctness proofs becoming mainstream.

Improve this answer
2
  • 8
    The halting problem says that we cannot determine if any arbitrary program halts. These programs can do weird things, like test every integer to see if it is a Mersenne prime. We don't do this in normal programs!
    – Casebash
    Sep 2, 2010 at 23:16
  • 1
    @Casebash, the question is whether there is a useful subset of programs for which the halting problem can be solved. Thats by no means clear either way. I.e. can we restrict our programs so that we can't do things like test every integer without ruining our ability to do useful tasks?
    – Winston Ewert
    Dec 22, 2011 at 20:43
1

It's already used by everyone. Every time you use your programming language's type checking, you're basically doing a math proof of the correctness of your program. This works already very well - it just requires you choose correct types for every function and data structure you use. The more accurate the type, the better checking you're going to get. The existing types available in programming languages already have powerful enough tools to describe almost any possible behaviour. This works in every available language. C++ and the static languages are just doing the checks in compile-time, while more dynamic languages like python are doing it when the program is run. The check still exists in all these languages. (for example, c++ already supports checking of side effects the same way haskell does, but you just need to choose to use it.)

Improve this answer
4
  • With the bit about side effects in C++, are you referring to const correctness?
    – Winston Ewert
    Dec 22, 2011 at 20:44
  • yes, const + const member function. If all your member functions are const, all the data in the objects is non-modifiable.
    – tp1
    Dec 23, 2011 at 5:24
  • They are still modifiable if you use mutable or const_cast. I certainly see the connection you draw there, but the flavor of two approaches seems rather different to me.
    – Winston Ewert
    Dec 23, 2011 at 6:00
  • Well, that's why you need to choose to use it -- there are always ways to go around it. But the important bit is how to make compilers check for problems in the area.
    – tp1
    Dec 23, 2011 at 6:23

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