Will correctness proofs of code ever go mainstream? [closed]

Question

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?

Answer 1

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

Answer 2

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

Answer 3

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!

Answer 4

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.

Answer 5

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

Answer 6

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

Answer 7

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.

Answer 8

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.

Answer 9

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

Answer 10

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