🚀 go-pugleaf

I argued that to reuse a software component, one must be able to see its
source code, and that it was a mistake to think that formal specifications
were going to solve the problem.

Bruce Weide summarized my argument as
(1) Writing formal behavioral specifications for components is hard.  
(2) A complete formal specification IS a program.  
(3) Smalltalk programs I has written look a lot like specifications I
    has seen.

It is always interesting to see how others interpret my words.
I don't think (1) is a crucial point.  (2) is crucial, and (3)
is just there to back up (2).  In fact, I don't think that Smalltalk
is at all unique in this regard.  For example, the first Ada compiler
was written in SETL and was really more of a specification for Ada,
or a design of an Ada compiler, than it was a "real program".  Although
it was executable, it only compiled a few lines per minute.

My last message elaborated on (2).  However, I've been thinking about
(1).  I'd like to say some provocative things.

First, to the best of my knowledge, nobody has written formal behavioral
specifications for a real component library.  There was a group at
Tektronix that was using Z to specify a few Smalltalk classes, and there
is a group here at Illinois that is using Z to specify a few classes
from a library of operating system classes written in C++, but neither
of these groups are dealing with more than a few classes.  There is
also the Larch group at MIT, though I haven't seen anything from them
dealing with real libraries.  It seems to me that the burden of proof
is on the side of those who claim that it is reasonable to expect to
have formal specifications for component libraries.  I would love to
be proved wrong.

I am not one of those who think that formal specifications are useless.
Quite the contrary, I demand that my students take courses in programming
language semantics and program verification, and I studied both when I
was in graduate school.  However, so far the effect of these topics on
computer science has been indirect.  They have helped us invent better
languages and learn to think about programming better, but they have had
little use in commercial programming.  Perhaps this will change soon, but
I see little sign of it.  There are too many unsolved problems, like how
to reason about pointers.  On the other hand, I am greatly in favor of
more research being done on the problem and wish that the area was
funded a lot better than it is.  It is an important problem, and one
worthy of the attention of many people, but it is an area that offers
many interesting research topics, not one that offers ready-made solutions
to current practical programming problems.

Ralph Johnson -- University of Illinois at Urbana-Champaign