Re: Silly and stupid post-condition or not ?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 3 Feb 2012 21:27:40 -0600, Randy Brukardt wrote:

> "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.

No, you don't need all information, but each piece you get must be complete
in itself. Informally, completeness is just about knowing the choices to
make.

> 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.

Quite so, but there still exist hard facts, which cannot be ignored without
being punished. 2x2=4, function is not a constructor (:-))

> Can I prove correctness? No, but that is not now and never will be a useful 
> goal.

I don't think so. As the amount and complexity of the software grows the
traditional means of ensuring software quality stop working both
technically and economically.

I see it on the example of GNAT compiler. Probably most experienced and
talented people in the world cannot get it right for about 20 years. 20
years is the age of one generation.

> If it was possible, it would just cause an infinite regress anyway.

True. You always need to take some things for granted. That is no problem
to me. This seems to be a problem to people from your camp: we cannot check
for Strorage_Error! Why? Of course you can, just let the programmer fill
the gaps, let proofs be conditionals. Any proof is conditional because of
that infinite regress. Why throwing everything away?

> 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.)

And again, this is what you get. If you refuse to integrate formal stuff
into the language, then, inevitably, an ugly modeling tool to come. And one
uglier on top of it and so on. Tools prey and feed on weak languages.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de