[e-lang] Skeptical words about formalization (was: Security is the
markm at cs.jhu.edu
Thu Jul 7 18:42:45 EDT 2005
Peter Van Roy wrote:
> According to John Allen [...] force software engineering to become a real
> engineering discipline instead of a hacker's paradise [...] formal semantics
I've been hearing this tune since I first got into computer science in 1975,
though the supposed forcing function keeps changing. I just recently reread
Dijkstra's 1972 Turing Award Lecture, in which he says the same thing, but
cites reliability and software development cost rather than security. Further,
he predicts that the formal methods revolution is just a small number of years
away, and that expensive unreliable software will shortly be a thing of the past.
I also just read for the first time Knuth's Turing award lecture, about why he
called his planned seven volume series "The *Art* of Computer Programming"
rather than "science" or "engineering". In it, he explores the history of
these categories over several centuries of human thought. The boundaries we
currently draw between these categories are not given, and there are many
other plausible ways of taxonomizing human activities of exploring and building.
Having come back to school after many years in industry, I'm impressed by how
much formal methods have advanced, and how many more problems formal methods
have now been successfully applied to. However, every small advance provokes a
new flowering of optimism that we're finally beyond the difficulties of the
past, and that the formal methods revolution is now, finally, this time, just
around the corner.
The formal methods revolution that has occurred is in the domain of academic
As more people enter the field, more people submit more papers in order to go
after increasingly scarce of top journals and academic positions. When demand
goes up faster than supply, some form of "price" bar must be raised until
accepted demand meets supply. Ideally, in academia, this "price" should be
quality of the ideas, and what a wonderful field our's would be if the quality
of ideas being published kept going up. However, judging quality of ideas is
hard. It's much easier to raise the formalism bar -- to add more formalism
hoops that papers need to jump through, just because fewer people are able to
do it. IMO, economics was destroyed by this same process, starting some 50
years earlier. Fortunately, economics is now starting to recover, so perhaps
someday our field may too.
Of course, formalism itself is quite valuable in both fields. None of what I'm
saying should be taken to imply otherwise. But it's easy to overestimate its
value, and it's especially easy to allow degree-of-formalism to displace other
often-more-appropriate metrics of quality.
> So where is the formal semantics of E?
A start at an attempt can be found at
<http://www.erights.org/e-impls/e-on-isabelle/Min_E.thy>. Having gone through
this exercise, I find it did not at all contribute to my understanding of
Kernel-E. Kevin Reid and Dean Tribble are both re-implementing Kernel-E. I
would not recommend that they or anyone refer to this document to help clarify
their questions about the definition of Kernel-E.
Rather, the existing Java implementation is slow largely because it's heart is
written to read like an executable specification of the semantics of Kernel-E.
Programming languages are, in some ways, good formalisms to express the
semantics of other programming languages.
> Where is the kernel
> language of E? Trying to define such a kernel language
> will point out lots of little problems, I'm sure of it!
The stale documentation that exists is at
<http://www.erights.org/elang/kernel/index.html>. The heart of the Kernel-E
implementation-as-executable-specification is in the "subEval" methods
implemented by subclasses of EExpr, and "testMatch" methods implemented by
subclasses of Pattern. Obviously, this state of affairs is intolerably ad-hoc.
However, at this stage, I think we could all benefit much more from careful
Guy-Steele-like technical documentation of Kernel-E's semantics -- together
with a rationale! -- than we would from bringing the above Isabelle theory
file to completion.
Text by me above is hereby placed in the public domain
More information about the e-lang