[plt-scheme] Perplexed Programmers

On Aug 29, 2007, at 6:01 PM, Marco Morazan wrote:

>> Like you, however, I have challenged Tony Hoare in public to
>> give me numbers of failures before he pushes his software
>> verification agenda one more time with a silly invited talk.
>> He was stunned hearing this challenge coming from me but
>> not one of the 60 attendees at the Federated Logic had a
>> good response and two voiced their support for my challenge
>> publicly.
>>
>
> Although I understand the need for numbers, why challenge the need for
> verification? Proofs often give rise to insights. They did for me in
> more than just a few occassions.

[I specifically challenged Tony's claim that software products
contain more errors than engineering products of the same kind
of complexity.]

Proofs and theorem proving gives teachers like us the insight
to produce good program design principles. See HtDP. I do not
think we have enough time to verify accounting programs like
the one at LA ISD. I don't think verification would catch this
kind of non-performance. The requirements engineers would
instead produce a verification claim that says the currently
existing program is correct. So I conjecture the problem is
smeared across the development cycle.



>> That's #1. And it is professionals like us who have failed to
>> bring across to the general public and to managers that
>> programming is not an 'idiot' job (though 'idiots' can write
>> things like programs for their own amusement and that nobody
>> else uses).
>>
>
> There may be a bit too much unfairness here. Is it possible that we
> have delivered the message, but that some have chosen to ignore it?
> There may be a bit of "just get anyone in here that claims to be able
> to deal with this" attitude out there.


The word 'like' in English means people who are in positions
like us but doesn't include us. The word such as would have
been all-encompassing. (See Bugs in Writing for an explanation
of this distinction.)

Even though, I accept your revision and agree that a few of us
have pointed out the problem -- but not all people in teaching
positions -- and that a lot of people have ignored this warning.

Responsibility is smeared across many individuals. Some give
their best, and some ignore the best (knowingly). But it rises
from there and goes on to groups. (Subsidiary)


>> #2 is that we have failures at an order of magnitude that
>> -- due to software's flexible nature -- can be made to look
>> like sufficiently partial successes that everyone accepts.
>
> Does this not beg for verification? Passing failures as successes
> seems to suggest the need for verification IMHO.


No, it calls for improved software construction processes.
Yes, it calls for the use of some verification technology
as if it were an advanced debugging aid. QuickCheck is an
example that comes to mind.

In general, verification is and remains to expensive for
mundane tasks.

-- Matthias