Re: What databases have taught me

Dmitry A. Kazakov wrote:

[ loads of snippola ]

> ... See Ada, which has it since 1983, and is
> one of the most strictly typed language, with the most carefully specified
> semantics.
>

Hmmm... I seem to remember someone trying to do a set of denotational semantics for Ada in the early 1980s, but they certainly had to give up on the concurrency side (I think they dropped out to operational semantics for that) and I'm not sure how many other bits they missed out.

That was to be the sum and substance of my response to that, as the notion that Ada had "the most carefully specified semantics" didn't tally in any way with my memory of the situation, but in a sense it gets both better and worse. Since the last time I concerned myself enough about Ada was over 15 years ago, I thought I ought to do a quick check on things. A quick Google turned up (among other advances in specifiying the semantics of smaller or bigger subsets of Ada) SPARK, a fully unambiguous subset of Ada, used to write provable software for critical applications. The white paper on the web site (http://www.praxis-his.com/pdfs/Spark_abstract.pdf) on the use of Abstract Interpretation includes the following passage :

"Precision is all about lack of ambiguity. All modern standard programming languages
(even Ada) suffer from ambiguity in their definition. For instance, in Ada the order of
evaluation of expressions and the parameter passing mechanism are not defined, to
allow the language to be reasonably implemented by a range of compilers for a range of
target architectures. This is perfectly reasonable, but creates a significant problem for a
static analysis tool. In the face of such ambiguity, a tool must either analyse every
possible option, or must make an assumption in choosing one of them."

Also remember that SPARK, while provable, is a subset and one of the original prescriptions for Ada was "no subsets" - hence the closing sections of Hoare's "The Emperor's Old Clothes" Turing Award speech.

And on a side note, another paper by the producers of SPARK, entitled "Languages, Ambiguity and Verification"
(http://vstte.ethz.ch/Files/spark.pdf) has the followng paragraph, regarding barriers to customer acceptance of static verification & proofs :

"... we often struggle to convince organizations to adopt the technology. The reasons are rarely technical, but seem to fall into the following general categories:
...
Snake-oil, wizards, gurus...
The software development industry is rife with approaches, -isms, tools, magics, and wizards-most of which fail to deliver all that they promise. Differentiating SPARK from this crowd remains a constant battle.
Secondly, some engineers are indeed very capable at working with imperfect technologies and processes, and produce excellent results. These "gurus" become the "heroes" of a project, and management come to depend on their skills and advice for this and future efforts. SPARK undermines these witch-doctors, and so we (ironically) find that the most talented engineers in an organization often find SPARK or similar approaches to be a threat."

(Of course, SPARK is a commercial product, and the above should have a certain amount of "they would say that, wouldn't they ?" caution applied - but I found this paragraph in particular quite appealing.) Received on Sat Jul 01 2006 - 09:51:40 CDT