🚀 go-pugleaf

I guess I don't really believe that "if certain
technical problems could be solved, there might be some hope for
substituting formal specifications for source code as descriptions of
component behavior."  That might be true, but it remains to be seen.

It is pretty hard to *prove* my opinion.  Even if we haven't
started using formal specifications a hundred years from now, the
solution might lie right around the corner.

So far, we have been debating my claim that there is not that big
a difference between specifications and programs.  My claim is
that our programming languages will improve to the point where
they let us write programs that are just like the specifications.
For example, the specification

f(x)=y, where y is in D and g(y)=x

can be written in Smalltalk as

D detect: [:y | y g = x].

I know the notation is a little wierd, but that's not the point.
The point is that it is POSSIBLE to write programs on the same
level as the specifications.  If D is infinite then the program
might not terminate, but I write infinite objects all the time
(i.e. the stream of all prime numbers).  Naturally, I tend to
reimplement these inefficient programs as time goes on, though
it would be possible to argue that what I am really doing is
starting with specifications and incrementally implementing them.
In fact, that's how I like to think about it.

The second point that I think is important is that most of the code
in a large system is not algorithmic, and is not amenable to this
kind of specification.  The specification of user interfaces, for
example, tends to look an aweful lot like the implemenation unless
you go to a lot of work to invent higher level concepts.  For example,
if you worry about exactly how the screen will look then the specification
is just a slow implementation.  On the other hand, if you introduce the
idea of "choices" and say that a particular "choice" can be made by a
"menu" then you can reason about the problem much more abstractly.
However, modern user interface management systems are moving in this
direction---they are making these specifications executable.

The third point is specific to object-oriented programming, which
I think is the best way to achieve code reuse.  One of the several
important ways to reuse software (some people seem to think this is
the only one o-o languages provide, which is wrong) is to inherit
a class and to override some of the procedures from it.  This ability
to override procedures is crucial---many classes are designed in such
a way that they cannot be reused until procedures are overridden.
It is possible to provide formal specifications of the procedures that
you expect will be overridden, but it turns out that it is very hard
to predict exactly what will be overridden.  A class is most reusable
when it is possible to override anything.  This means that every
procedure will be formally specified.  Since the median procedure size
in Smalltalk is 3 lines, this means that few procedures will have
formal specifications that are anything other than their implementation.
Thus, providing formal specifications is really the same thing as
providing the implementation.

I would like to advance a fourth argument, which is one that I have
not used before.  That argument is that almost all the design effort
goes into making the formal specification.  That is one of the reason
that formal specifications are so important.  They let you debug a
program at a high level, where it is easy to think about the problem.
Of course, I believe in programming at a high level, but lots of other
people seem to be content with C, and it certainly is a good idea for
them to design their system at a higher level and then translate it
into the lower level.  The effort in designing an object-oriented system
is defining the classes and their interfaces.  Once you give this away
to people, it is easy for them to recreate the code.  Thus, programs with
formal specifications are almost as easy to recreate as programs with
source provided are to understand.  This argues that formal specifications
are not going to be solutions to the problem of protecting the ownership
rights of the authors of the components.

Research in formal verification has had many influences on CS.  One of
the most important is that it has taught us what is difficult.  For
example, it showed that goto statements were hard to think about.
It also shows that pointers are hard to think about.  This is why
lots of modern languages, especially the symbolic ones, don't have
explicit pointers.  However, the effect is for programming language
designers to borrow good ideas from the specification people.  I
think that the future will lie in that direction.

Ralph Johnson -- University of Illinois at Urbana-Champaign