piclist 2009\02\06\085645a >
Thread: Agile programming (was Re: [P|C] Banksel)
face picon face 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.
<001501c98862$d011f4a0$0300a8c0@main> 7bit

See also: www.piclist.com/techref/microchip/devprogs.htm?key=programming
Reply You must be a member of the piclist mailing list (not only a www.piclist.com member) to post to the piclist. This form requires JavaScript and a browser/email client that can handle form mailto: posts.
Subject (change) Agile programming (was Re: [P|C] Banksel)

month overview.

new search...