Subject: Re: Can you learn computer science from a school?
From: (Rob Warnock)
Date: Sat, 19 May 2007 23:52:29 -0500
Newsgroups: comp.lang.lisp
Message-ID: <>
John Thingstad <> wrote:
| Rob Warnock <> 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,


[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			<>
627 26th Avenue			<URL:>
San Mateo, CA 94403		(650)572-2607