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.
-- 
http://www.piclist.com PIC/SX FAQ & list archive
View/change your membership options at
http://mailman.mit.edu/mailman/listinfo/piclist