[plt-scheme] Perplexed Programmers

On 8/29/07, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> 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

But it may do more than that. The process of proving a program correct
can reveal subtle errors in coding or in the "logic" behind the
algorithm being implemented. I am not suggesting that very line of
code written requires verification. What I am suggesting is that
verification can be useful in the software development cycle.

(BTW, did you really mean to use "like" above or would "such" had been
a better choice? ;-)

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

Point taken although the distinction is a bit subtle. (see side comment above)

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

Agreed. If individuals give and demand the best, then groups up the
chain will also.

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

OK, I believe we agree in general. Verification can/does play a role
in the software construction process.

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

At the risk of being flamed, we should not be verifying the obvious
nor is it reasonable to verify every line of code.

Cheers,

Marco