[plt-scheme] Perplexed Programmers

From: Marco Morazan (morazanm at gmail.com)
Date: Wed Aug 29 18:48:25 EDT 2007

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.



Posted on the users mailing list.