Re: Silly and stupid post-condition or not ?

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:143dxzgfasd4o$.a7lekw80xee2$.dlg@40tude.net...
> On Thu, 2 Feb 2012 21:13:04 -0600, Randy Brukardt wrote:
>
>> I've always hated the emphasis on completeness of these things, because 
>> it
>> is *exactly* the wrong approach to getting something in wide-spread use
>> (even in the Ada community).
>
> Putting my hat of logicians on: you can't get anywhere without
> completeness. This is how logical inference rules work. Sorry for that, 
> but
> there is no other way.

That's complete and utter bunk. As a compiler writer, I know that a compiler 
can prove all kinds of useful things knowing very little about the program 
in question. And moreover, any information that the compiler can gain is 
helpful; it does not have to be complete in any sense.

The problem here is that people have allowed themselves to be tied in knots 
by formal theories, when it's obvious that you can do plenty with nothing 
but some computing power and a bit of Boolean logic. Formal theories are 
hardly worth the paper they're written on.

Can I prove correctness? No, but that is not now and never will be a useful 
goal. If it was possible, it would just cause an infinite regress anyway. 
Specifically, if you can specify the behavior of a program well enough that 
you can prove 100% of its semantics, then the effort to write the actual 
program was wasted (at least in the vast majority of programming tasks) --  
you would have been better off directly executing the specification. And 
pretty soon, people will be doing that, and we'll be back to having no 
proofs of any kind. (And a much harder to understand specification on top of 
it.)

What I can prove is the presence of some bugs and the absence of other 
behaviors (like raising an exception). And for almost all uses, that's 
enough.

Formal completeness is *always* the wrong goal.

                                                   Randy.