www.piclist.com/techref/microchip/devprogs.htm?key=programming

BY : email (remove spam text)(Olin Lathrop)

Sean Breheny wrote:

> I'm not sure what type of "provable" you mean. There is very much an

> ongoing effort in CS and engineering circles to have programming

> languages for which one can automatically prove that functions do what

> they are intended to do for all inputs. In other words, if you have a

> programming language which is restrictive enough (for example, does

> not allow intercommunication between functions except by explicit

> parameter passing), you can then state the proposition that function

> "CountWidgets(x)" always returns the correct value for any x in the

> set of integers. This proposition can then be fed to an automatic

> theorem prover program which can produce a mathematical proof that the

> proposition is true (or false, or perhaps unable to determine).

All you're doing is pushing the human error to whatever input the prover

needs. At some point a human is going to have to describe what he wants,

and that's the point at which screwups will always happen.

In your example, you may prove that CountWidgets does indeed perform the

stated function correctly. But what if the error is that you're only

supposed to count blue widgets, not all of them, or the super sized widgets

are supposed to be counted double, etc, etc, etc?

All this correctness proving seems so pointless because it can only prove

the correctness of trivial code, and then only what you said it's supposed

to do, not what it's really supposed to do.

********************************************************************

Embed Inc, Littleton Massachusetts, http://www.embedinc.com/products

(978) 742-9014. Gold level PIC consultants since 2000.

See also: www.piclist.com/techref/microchip/devprogs.htm?key=programming