Weblogs Forum - Can Provably Correct Code Exist?

Articles |
News |
Weblogs |
Books |
Forums

Artima Forums | Articles | Weblogs | Java Answers | News

Sponsored Link •

Weblogs Forum
Can Provably Correct Code Exist?

14 replies on 1 page. Most recent reply: Jul 29, 2006 1:56 PM by Andy Dent

Welcome Guest
Sign In

Back to Topic List

Reply to this Topic

Search Forum

Threaded View


Previous Topic		Next Topic

Flat View: This topic has 14 replies on 1 page

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Can Provably Correct Code Exist? (View in Weblogs)

Posted: Jul 23, 2006 3:41 PM

Summary
Yes and no.

Is there truly such thing as provably correct code? Even though some code can be proven to be correct with regards to a specific specification, what guarantees that specification to be correct? The solution and the challenge go on ad infinitum without resolution.

On the other hand code can be viewed as always correct, if you take it to be its own specification.

How do you like them apples?

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

V&V

Posted: Jul 23, 2006 4:07 PM

Andreas Mross

Posts: 12
Nickname: amross
Registered: Apr, 2004

Re: Can Provably Correct Code Exist?

Posted: Jul 23, 2006 5:59 PM

The answer is no.

I remember learning about this at uni, in the "Theory of Computation" subject. Unfortunately I can't remember the details :-) I remember something about the Halting Problem and NP Completeness etc... it was actually my favourite subject at uni. Unfortunately, the number of opportunities I have had to use any of it in my career is currently zero :-)

There has been a lot of research done in this area.

Malte Finsterwalder

Posts: 20
Nickname: jufoda
Registered: Aug, 2003

Re: Can Provably Correct Code Exist?

Posted: Jul 24, 2006 12:32 AM

> The answer is no.

The answer is yes.

Computing theory only states that it's impossible to prove every code correct. But it sure is possible to prove a lot of code to be correct, if you put some brain and effort into it.

The real ploblem is, as stated before: You can only prove that the code fulfills a formal specification of your problem. You can't prove that the specification really solves the problem the people want solved.

Is proving thus useless? I don't think there is a yes or no answer here. It depends on the situation.

If we were to prove our code, we would reduce all the exidential bugs from it. That would still be great.
We couldn't reduce the misunderstandings in the spec, but that's another story.

Greetings,
Malte

Joao Pedrosa

Posts: 114
Nickname: dewd
Registered: Dec, 2005

Re: Can Provably Correct Code Exist?

Posted: Jul 24, 2006 2:03 AM

Remove the error-prone humans from the equation. :-)

Christian Sell

Posts: 2
Nickname: csell
Registered: Jun, 2003

Re: Can Provably Correct Code Exist?

Posted: Jul 24, 2006 4:19 AM

You can only perform a proof against a specification, as the intial poster pointed out. However, If you have a truly correct, unambigous and complete specification, there is no point in writing a program by hand - a generator should do that.

This demonstrates the fact that a compilable (generateable) program is a (the most detailed) form of specification, and you obviously cannot prove a statement against itself.

nes

Posts: 137
Nickname: nn
Registered: Jul, 2004

Re: Can Provably Correct Code Exist?

Posted: Jul 24, 2006 9:21 AM

> You can only perform a proof against a specification, as
> the intial poster pointed out. However, If you have a
> truly correct, unambigous and complete specification,
> there is no point in writing a program by hand - a
> generator should do that.
>
> This demonstrates the fact that a compilable
> (generateable) program is a (the most detailed)
> form of specification, and you obviously cannot prove a
> statement against itself.

Bingo! I wish more people would realize this. Unfortunately most high-level (domain specific) language implementations are not nearly as good at finding an efficient solution to a specification as they are at finding a correct one. Since we can check lower level abstractions with details we know about the higher level ones, what ends up happening is that we write a lower level spec and then check that against a higher level spec, doing the extra work for performance reasons.

It is possible to automate some of that by reducing the solution domain space using, for example:
Domain aware program checkers that will warn about suspicious code of the type “you should check this because we usually don’t do that here”.
“Meta-annotations” (e.g. type information, invariants) that will restrict what kind of code is considered valid.
Specific tests that must pass.

One problem is that although higher level specifications change more slowly, they do change! That often means that we start fighting the checkers and tools instead of adapting them in light of the change.

Coman Horia

Posts: 3
Nickname: bonzai
Registered: Jul, 2006

Re: Can Provably Correct Code Exist?

Posted: Jul 24, 2006 9:57 AM

You should also consider the abstractness of a program when speaking about corectness. Certainly a Haskell procedure is easier to prove correct (or something of the kind) than a Assembler chunk of code.

Andy Dent

Posts: 165
Nickname: andydent
Registered: Nov, 2005

Re: Can Provably Correct Code Exist?

Posted: Jul 24, 2006 5:17 PM

Correct is not binary. I think Can Provably "Good Enough" Code Exist? is a more useful and interesting question.

Buried in the idea of conforming to a specification is the fact that a lot of data is sloppy.

In areas such as geological data, where I do a lot of work, data can be sloppy or trusted in the sense of :
- known measurement accuracies of instruments used
- accuracy of techniques used (not the same thing as instruments, numerical post-processing may be revised down the track but if you don't have the raw data, this is a layer of inaccuracy)
- reputation of responsible party

Richly attributed data such as the XML-based models we use allows you to annotate raw values with such subjective judgements about suitability, as well as more straight-forward units of measure and significant digits.

One of the key drivers for CEDSimply is the search for a language or need to define one, that can work with this good enough concept.

piglet

Posts: 63
Nickname: piglet
Registered: Dec, 2005

What's god enough?

Posted: Jul 25, 2006 7:03 AM

Now I'm curious how you define "good enough", and how you attempt to prove "good enoughity".

Vladimir Nesov

Posts: 27
Nickname: robotact
Registered: Aug, 2005

Re: Can Provably Correct Code Exist?

Posted: Jul 27, 2006 3:10 AM

For such question there should be a definition of "correct" attached.
If we would be able to write code (in practice) that is provable to behave according to common types of thinkable specifications, it'd be greatest milestone by itself. Imagine that tests as they are now would be written in more abstract form, not requiring straightforward runnability, like "apply method to this domain and check results", would that be nearer to "correct"? Problem with tests is that they test only single state, when in principle there's specification potential for more.

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Specification can not be proven correct, code can.

Posted: Jul 28, 2006 2:56 AM

> Is there truly such thing as provably correct code? Even
> though some code can be proven to be correct with regards
> to a specific specification, what guarantees that
> specification to be correct? The solution and the
> challenge go on ad infinitum without resolution.
> <p>
> On the other hand code can be viewed as always correct, if
> you take it to be its own specification.
> <p>
> How do you like them apples?

Specification can not be proven correct, code can.

First of all, code IS specification. It is just that code is a lower level specification than specs.

In order to prove code correct, you have to check it against specification. If it conforms to all the constraints of the specs, then it is correct.

But how can you prove the specs correct? you need another set of specs, that are even higher level, to prove the initial specs correct.

And then how do you prove the higher level specs correct? you need an even more higher level specs.

The conclusion is: for each level of specification S, you need another level of specification S' that proves S correct.

This means that code can only be proven relatively correct, unless there is a specification U that is provable by itself; that would be the ultimate specification (thus the U term). Then the code would be absolutely correct.

Kay Schluehr

Posts: 302
Nickname: schluehk
Registered: Jan, 2005

Re: Specification can not be proven correct, code can.

Posted: Jul 28, 2006 3:30 AM

> Specification can not be proven correct, code can.
>
> First of all, code IS specification. It is just that code
> is a lower level specification than specs.

Hmmm... this does not make much sense to me. Just specify what a sorting algorithm on a list of integers ( or an arbitrary list type eqipped with a partial order on its elements ) shall do. Than prove constructively that a certain algorithm actually does what the specification asserts. The algorithm is nothing but an existence proof of the underlying assertions of the spec. It might me implemented on a machine or not. Handcrafted proofs are done by mathematicians for centuries. The spec can be completely nonsensical, impossible and contradictory and so any program/proof will fail.

Theorem provers just force the programmer to specify the assertions formally such that they can be derived from facts presented to the system. Instead of showing that a certain algorithm can be used to prove the spec the algorithm is replaced by another algorithm that can derive assertions mechanically. I don't want to comment on the practice of using theorem provers because I never used any and I don't plan to use one in future.

Paul de Vrieze

Posts: 9
Nickname: pauldv
Registered: Oct, 2005

Re: Can Provably Correct Code Exist?

Posted: Jul 28, 2006 1:13 PM

> The answer is no.
>
> I remember learning about this at uni, in the "Theory of
> Computation" subject. Unfortunately I can't remember the
> details :-) I remember something about the Halting Problem
> and NP Completeness etc... it was actually my favourite
> subject at uni. Unfortunately, the number of opportunities
> I have had to use any of it in my career is currently zero
> :-)
>
> There has been a lot of research done in this area.

The halting problem is not necesarilly a problem for the existance of provably correct code. It precludes all code from being provably correct.

There is still a lot of research done in the area. A more interesting question however is what correctness is. And where do you put the boundary. If you are very strict and only accept certainty that computer X will do exactly as intended by the designer you're out of luck. While digital computers are rather reliable, they are not 100% reliable, so your software is not going to be executed error free in 100% of the cases. These errors do happen. Especially with memmory or with unsufficient power supplies, but can also happen (a lot less frequent) because of cosmic rays.

In a less strict way, correctness is still bound to the question of completeness of the specification. If one wants to prove that an application does what is intended one needs to know that the specification to be tested against is complete as well as correct. Intuitively the completeness is unprovable, but I could be wrong there.

Andy Dent

Posts: 165
Nickname: andydent
Registered: Nov, 2005

Re: What's god enough?

Posted: Jul 29, 2006 1:56 PM

> Now I'm curious how you define "good enough", and how you
> attempt to prove "good enoughity".

Good enough, like beauty, is in the eye of the beholder :-)

From a roadshow I was involved in last year, If the data you've got is sh*t, tell me it's sh*t, but still give me the data (Aussie audience of geologists and miners.)

So good enough has to be qualified by the standards of the user as they were at a given point in time. That can involve a whole series of questions, along the lines of what might be required to justify a decision in a court of law:

- what is the chain of custody of the data?
- are the measuring devices currently certified?
- desired accuracy for user - someone might just make decisions based on the binary pattern of data being available at given locations, rather than the values. ("Show me places where someone has NOT looked for Gold.")

Flat View: This topic has 14 replies on 1 page

Previous Topic

Next Topic