Re: Undefined behaviour [was Re: The D Programming Language]
James Kanze wrote:
Andrei Alexandrescu (See Website For Email) wrote:
James Kanze wrote:
Java has no acknowledged undefined behavior. Unless you
consider that its inventors were divinely inspired, and somehow
protected from the errors which the rest of us make, whether it
be in programming or in writing a specification, you should be
sceptical of such claims.
This is wrong. Please, let us try to make statements when they are
backed up by knowledge.
Well, I have specific knowledge that the Java specification was
written by human beings. And while I cannot prove it, my
experience gives me very strong reasons to be believe that human
beings are not perfect.
I'm nonplussed. Anyone is free of course to believe what they want. One
could even believe that some theorem is not true because it was created
by humans, etc. But as long as anyone lacks means to substantiate their
belief, that belief better be expressed as such, and not as the truth.
The comment about human beings being imperfect is, of course, an
invitation to fallacy that we can leave out of the discussion. Please.
It is well understood how to define languages that have no undefined
behavior. That can be proved mathematically (using formal logic). The
proof includes two parts: progress and preservation. Progress proves
that a well-typed program in any state will make a step. Preservation
proves that whatever step a program takes, it will stay well-typed.
Together, these two proofs complete the type safety proof of a language.
And what relationship does that have to not having undefined
behavior? A language can be perfectly type safe, and still have
undefined behavior.
Wrong. Progress and preservation together prove soundness - that is, any
program in the language will execute a defined action while staying
typesafe.
But of course, your statement begs the question anyway. You now
have to prove that the proof is correct, and more importantly,
complete. Unless you have divine revelation for that. (Note
that the "complete" is the tricky part. If you forget to define
some behavior, you have undefined behavior. If you forget to
consider certain steps in your proof, you're proof is not
complete, and the language may have undefined behavior.
This is another invitation to fallacy. Then we'll have to prove that the
proof of the proof is correct, and the door is opened for infinite
regression.
Proofs are mechanical and based on formal logic axioms. They have been
looked upon many people who assessed their correctness. I'm not sure you
want to base your argument on "but they could be all wrong."
The "proof may be incomplete" argument does not hold, but in order to
discuss why it doesn't hold, more background would be needed. I suggest
again that perusing "Types and Programming Languages" would be a wise
thing to do. This sounds rather snooty, but isn't it nice when people
build competence in things they enjoy discussing?
This
is, for example, where the original Java specification failed
with regards to the case I raised.)
Could you please detail this?
For more details, see "Types and Programming Languages" by Benjamin Pierce.
Single-threaded and reflection-less Java has been proven to be typesafe
in 1999. The proof operates on a small core of Java (called
Featherweight Java) for proof size reasons. See
http://citeseer.ist.psu.edu/igarashi99featherweight.html.
I don't know whether similar formal proofs have been made for
multithreaded programs, but
http://www.cs.umd.edu/~pugh/java/memoryModel/semantics.pdf seems to do
exactly that (using a notation that I don't know). At any rate, it is
commonly considered that Java has gone farther than most languages in
defining semantics of multithreaded programs.
Understanding and dealing with such concepts entails long, unrewarding
work. (I suck at it and would at most be able to sweat my way through a
paper, but never to produce one.) But it is self-understood that an
unwillingness to get acquainted with some theoretical concepts that have
little practical utility at best, comes together with some restraint
when it comes about peremptory statements.
I'm not sure I agree. Because I'm using the language
pragmatically, in a concrete implementation. I'm aware
(vaguely) that there are numerous techniques of such proofs, but
as you point out, "[they] operate on a small core of Java". The
problem with language features is that they interact. Proving
each individual feature doesn't buy you much. And applying the
proof to the entire language has two problems: the techniques
being used generally don't scale well, and you still have to
prove that you haven't forgotten any feature, and haven't failed
to consider any combination of features.
Wrong. Proofs focus on a small core of the language do not lose generality.
They're along the same lines as
claims that a non-trivial program has no errors.
Program verification is known to be intractable for even simple
programs, unlike typechecking. So the comparison does not make sense.
If simple typechecking were sufficient to ensure no undefined
behavior, you might have a point (and even then, I'm not
convinced).
This is a misunderstanding, by a mile. It's not about typechecking. It's
about semantics. Semantics has to do with what each operation defined by
the language does. Types are an integral part of progress and
preservation because the proofs rely on the fact that the program
typechecked in the first place, to show that it always makes a step, and
to a program that remains typed.
At any rate, you're free to believe what you want here, because
as far as I can see, it has no practical implications.
I guess I could say the same. :o) All I'd like is that public false
statements were not made in a peremptory manner, and in ways that make
negation impossible because of refusal to acquire the needed background.
It's just wrong.
Andrei
--
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]