Re: virus: Brain Tennis

zaimoni@ksu.edu
Mon, 28 Oct 1996 14:03:32 -0600 (CST)


On Fri, 25 Oct 1996, David Leeper wrote:

> Kenneth Boyd,

[CLIP]

> > If one can prove that the source is bug-free, the only source of bugs is
> the compiler.
>
> Proving code to be correct? The only thing I've ever read about this is
> Dykstra'a "Predicate
> Calculus And Programming Semantics", a deep book to say the least. Is this
> what you're
> refering to? By the way, programs are memes, so its OK to talk about them
> on this list.

That is one of the two sets of techniques usable for that purpose, and
the one I'm more familar with. Another basis for such an approach is a
highly concrete lambda-calculus. I don't use this, from lack of
awareness. Some features of this, however, are incredibly useful to mimic
when designing class hierachies in C++.

Unfortunately, the procedure is inherently "bottom-up". It is much
better suited to a structured data-centric programming style than a
structured procedural programming style.

//////////////////////////////////////////////////////////////////////////
/ Towards the conversion of data into information....
/
/ Kenneth Boyd
//////////////////////////////////////////////////////////////////////////