Eiffel (Re: problems/risks due to programming language)

[Nick Rothwell]

In article <264 at eiffel.UUCP>, bertrand at eiffel (Bertrand Meyer) writes:
>    Every once in a while someone ``discovers'' that the Eiffel type
>system is ``wrong''. The latest printed occurrence I know of is a letter
>published in the last JOOP.
>
>    The Eiffel type system is neither ``shakey'' nor wrong.
>...
>    Denying the validity of Mr. Rothwell's statement would be
>contradicting a matter on which he is better informed than I am:
>his personal opinion regarding the Eiffel type system.
>There is no reason to doubt that the statement is true,
>although it provides information about Mr. Rothwell, not about Eiffel.

...touche... :-)

I didn't make the claim that the Eiffel type system is "wrong".
My statement was that it "seemed shakey" to me; I've only read
the Software Construction book, which does not seem to give a
good description of the type system. It may well be perfectly
sound, and there may be other literature proving its soundness,
but I was less than convinced based on my reading of the book.
Perhaps I shouldn't have aired my views in public.

>    Unfortunately for the theoreticians, the Eiffel rule is the one that
>makes sense in practice. To take a very simple example, take the generic
>class

Unfortunately, such statements do nothing to improve people's faith in
the soundness of the type semantics. A thorough, semantic description
of the type system would go a long way to banishing people's fears
(mine included).

>5. I have known for a long time Luca Cardelli's elegant work
>(A Semantics of Multiple Inheritance, in Semantics of Data Types,
>edited by Gilles Kahn, David B. McQueen and Gordon Plotkin,
>Lecture Notes in Computer Science 173, Springer-Verlag, New York,
>1984, pp. 51-67). This denotational model of some of
>the properties of inheritance suggests a contrapositive rule.
>Enamored as I may be of denotational semantics, however, I think that in
>science theories should be made to fit reality, not the other way around.
>Physicists are not supposed to change experimental results which do not
>agree with the model.

Could you explain what you mean here? The analogy with physics
is not really valid; I don't see why a theory should be built
to explain an existing (and perhaps totally ad-hoc) language;
why not design a sound type system and implement a language which uses
it?

>-- Bertrand Meyer

		Nick.
--
Nick Rothwell,	Laboratory for Foundations of Computer Science, Edinburgh.
		nick at lfcs.ed.ac.uk    <Atlantic Ocean>!mcvax!ukc!lfcs!nick
~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~
      A prop?   ...or wings?      A prop?   ...or wings?      A prop?