Re: What databases have taught me

On 1 Jul 2006 07:51:40 -0700, Tony D wrote:

> 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

Right, but note that side effects in functions aren't welcome. Programs exploiting the evaluation order of side effects are considered erroneous. This is not checked, though.

> and the parameter passing mechanism are not defined,

Same as above. Programs relying on passing mode are illegal. Aliasing is difficult to check anyway.

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

True

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

Right, you have to choose between an ability to prove and some language constructs. There are many applications, which alas, cannot be developed in SPARK, or the Ravenscar profile. This does not directly related to whether the semantics is well or ill defined.

Though overloading in result types does not expose any problems to either static checks or semantics.

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

I can sign to each word of this.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de