Position paper for the 21st Century Engineering Consortium Workshop

Pierre Flener, Ph.D.,
Bilkent University
Dept of Computer Engineering and Information Science
February 1998

     I attended (as a PC member & author) the ASE'97 conference and
listened with much interest to all interventions at the education panel.
Unfortunately, time was tight both during the panel (there was only time
for the panelists)and after the panel (because the conference then was over
and most people "disappeared" quite quickly).  I am personally deeply
interested in educational matters around (automated) software engineering
and (in)formal methods, and have 4 years of teaching experience in this,
and want to make the following participation to the "21st Century
Engineering Consortium Workshop", which I will not be able to attend.

     I concur with much of what was said at that panel, though not with
everything. But let me first explain my background (see my homepage -- URL
above - for more details): after my Ph.D. at UC Louvain (Belgium), I moved
to a promising upstart private university (called Bilkent -- The City of
Science) in Turkey, where I have carved out a niche for (automated)
software engineering related courses, namely:

	CS 322  Program Verification (junior year)
	CS 454  Software Engineering (senior year)
	CS 517  Automated Software Engineering (grad level)

     (The only other ASE courses I know of are the one at Stanford, and the
one by Dr Gordon Novak, at UT Austin.)  My students are all among the
finest in the nation (they all rank among the top-250 in the national
placement exam, which is taken by about 1.4 million candidates), and I tend
to get some of the highest teacher evaluation marks in the Engineering
Faculty.  I say this not to boast, but to stress the pertinence of my
following remarks.  So here is my position on formal methods education
(this position does not in any sense reflect the opinions of my employer):

     As much as I agree that significant changes in the way software
engineering is practiced in industry are needed, I am also deeply skeptic
whether formal methods are _the_ way to go!!!  Indeed, I have been unable
(yet) to work out a satisfactory way of teaching such things, and have in
my visits of other Euro/US departments never seen it done right either:
most students come out dazzled by such courses, seem to know less than
before, and are unwilling to apply it in practice.  With good reasons, I
believe!  (Please don't dismiss me as a lunatic right now, but bear with
me, because there is so much to say, and you will have to read my whole
argument before judging it.)  Formal methods tend to obstruct the really
important issues of software engineering, in favor of those that are
amenable to formal treatment (otherwise, no publications with Greek
letters, i.e. no promotions or tenure).  I believe `formal methods' is a
big misnomer, unless `formal' really means `formal' (i.e. based on the
usage of languages whose syntax & semantics are fully predefined), but this
would in turn be a big disaster for s/w engineering.  There was a large
number of (to me) "dangerous" people at ASE'97, who seemed to claim that
the only way for a specification/requirement to be precise would be for it
to be formal: I couldn't disagree more!  The phrase `formal specification'
is a contradiction in terms, as I explain with a Belgian co-author in a
paper, which is to appear in March '98 (?) in the Journal of Systems and
Software, Special Edition on Formal Methods Technology Transfer:

                                 Specifications Are Necessarily Informal
                                or: Some More Myths of Formal Methods

                       Baudouin Le Charlier (University of Namur, Belgium)
                                Pierre Flener (Bilkent University, Turkey)

   "We reconsider the concept of  specification  in order to bring new
insights   into the debate of formal versus  non-formal  methods in
Computer Science.   In  our  view,  the  correctness  of a  useful  program
 corresponds to an  objective  fact,  which  must have a simple,  precise,
and understandable  formulation.  As a  consequence, a  specification  can
(and must) only make precise the link existing  between the program
(formality) and its purpose  (informality).  Moreover,  program
correctness can be argued only by means   of  non-formal  reasonings,
which should be as explicit as possible. This   allows us to explain  why
specifications  cannot be  written in a strictly   formal language.  Our
view of specifications  does not imply a rejection of   all  ideas  put
forward  in  the  literature  on  formal  methods.  On the contrary, we
agree with the  proponents of formal  methods on most of their   arguments,
  except   on  those   following   from  the   assumption that
specifications  could (or  should) be formal.  Finally, we examine why the
role and nature of specifications are so often misunderstood."

     You can retrieve it as
http://www.cs.bilkent.edu.tr/~pf/pub/infspecs.ps.z   or email me if you
have trouble downloading it.  [Note that this version is not entirely
final, a few lines may change until publication.]

     The argument is lengthy, but compelling to anybody who really wants to
understand the underlying issues.  Careful, we do not pretend formal
methods are useless, only that the _real_ issues in software engineering
are about real (informal) specifications, and that formal methods research
can only help in producing some forms of "compilation" of very-high-level
formal languages into lower-level formal languages, or in checking internal
consistency & completeness properties of formal texts (to the exclusion of
external consistency & completeness properties, thus);  but note that
somebody, somehow, has to come up with such inputs to formal methods tools,
which issue is nearly always (conveniently?) overlooked by formal methods
proponents, although it is the key issue to successful software engineering
(but not amenable to formalization and thus regrettably considered
`uninteresting' by most researchers).  What's more is that I/we consider
formal methods to be extremely-long-term research at this point and thus
immature for introduction into undergrad curricula or industry (most tools
"explode" on all but the smallest toy problems).

     I teach my courses informally (i.e. like mathematicians, i.e. with no
usage of predefined languages whatsoever) and am quite happy & successful
with it, according to my students (they are of course too inexperienced to
compare).

Consider me "dangerous" now, or not, and please read my whole argument,
including the cited paper, but I am just worried that said workshop become
a slamfest of pro-formal-methods people (like many people at ASE'97) and
that those of us who are skeptic (and there are others) are not given a
voice.  I just wanted to beg for caution against a headlong rush into
formal methods, even though there is plenty interesting work going on there
(and I'm active there myself !).


[Comment from Dr. Michael Lowry: 
I think that the position of most at ASE'97 is that the essence of SE, now
and in the future, is to transform informal requirements into formal
artifacts.]


[Reply by Prof. Flener:
I hoped so, but maybe I talked & listened to the wrong people? That Italian
natural-language-requirements guy felt the same thing as I, namely that
there was some "aggressiveness" against everything informal.  Some people
almost literally jumped up as soon as they heard things like "informal
specs" and they went on to say that only formal specs can be
precise/unambiguous/etc, which is (as argued in that mentioned paper)
completely wrong and even a counterproductive attitude.  The existence of a
formal semantics is just eye-wash unless the formal text is grounded into
real life.  My ASE co-author Kung-Kiu Lau always praises formal semantics,
and we have wonderful "fights" about this, but it doesn't prevent us from
working together, because we have the same goal, the one you mention.]


[Comment from Dr. Michael Lowry:
 Today, the formal artifact is usually just the code - which has a precise
operational semantics. Unfortunately, in developing code, one has to do a
lot more than just develop a formal representation of the (informal)
problem one is trying to solve. The situation is like that of, say, a
control engineer - what if they immediately went from a control problem to
an analog circuit for controlling a device? (Ignore for the moment that
most control is now digital). This is how engineering was practiced in
ancient times.]


[Reply by Prof. Flener:
Indeed.  Well said.]


[Comment from Dr. Michael Lowry:
 In modern engineering, between the informal problems and the system, there
is a hierarchy of formal abstractions mediated by mathematics, usually
supported by automated tools. We are trying to do for SE what has already
been done in most other engineering disciplines.]


[Reply by Prof. Flener:
I agree on this objective.]


[Comment from Dr. Michael Lowry:
 While a priori you might think that the major benefits will only be
compilation and consistency checking, I believe the results could be much
more profound, matching if not exceeding what Prof. Newton indicated has
been done for digital hardware design.]


[Reply by Prof. Flener:
We will see.  As for me, I hope for this, but am also skeptic.]