``` Subject: Re: Can you learn computer science from a school? From: rpw3@rpw3.org (Rob Warnock) Date: Sat, 19 May 2007 23:52:29 -0500 Newsgroups: comp.lang.lisp Message-ID: <Sc-dnaPar86QSdLbnZ2dnUVZ_oOknZ2d@speakeasy.net> ```
```John Thingstad <john.thingstad@chello.no> wrote:
+---------------
| Rob Warnock <rpw3@rpw3.org> wrote:
| > The good news, such as it is, is that the Dijkstra proof methodology
| > is one of the few I've seen ... which handles imperative constructs
| > ... almost as conveniently as purely functional constructs.
|
| The bad new is that finding loop invariants is fairly difficult with
| the imperative constructs (Hoare logic)
+---------------

Quite true, in the general case.[1]  Fortunately, almost all the loops
one tends to write in "normal" code have a small set of loop-invariant
patterns that work well. ["Normal" loops being those more-or-less-simple
traversals or convergences where mostly all you have to worry about
are getting the boundary conditions right (avoiding "fencepost" errors),
where writing the loop invariant is a matters of seconds or a few
minutes at most. "Hairy" loops, then, would be those occasional monsters
where finding a suitable loop invariant is a matter of hours or days
(or forever!).]

+---------------
| You might bet better off specifying the system using Generator Induction
| logic and then, if necessary, transforming it to a imperative design.
+---------------

Haven't run across Generator Induction Logic yet. I'll look it up,
thanks!

-Rob

[1] I am reminded by this of the case of Shannon's Coding Theorem,
which *proves* that for any channel, no matter how noisy, there
*does* exist a block code which allows you to transmit data
as close to the channel capacity[2] as you like with as low
an error rate as you like, *BUT*... not being a "constructive"
proof, gives you absolutely *no* hints as to how to find said code.

Integral calculus sometimes feels like this, too.

[2] Note that the "channel capacity" is a function of *both* the
bandwidth (or bit rate) and the error rate, and decreases
with the error rate, thus this is not as impossible a promise
as it may sound initially.

-----
Rob Warnock			<rpw3@rpw3.org>
627 26th Avenue			<URL:http://rpw3.org/>
San Mateo, CA 94403		(650)572-2607

```