[e-lang] Skeptical words about formalization (was: Security is the Turning Point?)

[Mark Miller]

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 
publication.

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

     Cheers,
     --MarkM