This is the mail archive of the mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: [PATCH] C undefined behavior fix

<<I can think of a bunch.  Algol 68 is perhaps the most prominent
example (interesting, for one thing, because a lot of C++ features
were inspired by Algol 68).  PL/1 perhaps (at least when you consider
the IBM Zurich research lab work, I don't remember the author's name).
And the ANSI APL standard appears to be pretty close.

It is not clear what a *formal* language means. Formal is a word that
can have many meanings, and what we are really talking about is levels
of formality. The algol-68 report (I am one of the relatively few people
who at least at one time 100% understood the A68 report) has a formal
mathematical definition of the syntax and static semantics, but the
dynamic semantics uses formal english, and I really don't see a big
distinction between A68 and Ada (or even C++). Also, being mathematically
formal does not necessarily mean being more accurate or more precise (indeed
a drawback with many mathematical formalisms, as with formal specs in general,
is that if they get too wrapped up in mathematical notations, then they a
are hard to review). The EEC spent over a million dollars generating a
formal definition of Ada. I still have my copy, it is two giant telephone
books of mathematical formulae and it is close to useless. In particular
it skips the hard parts. 

Consider recent threads here under the above subject line, on volatile
and memory mapped-IO, and on how closely arithmetic must adhere to the
intent of the IEEE standard. These are the tough issues in defining a
language, and mathematical formalism is not a magic bullet for achieving
accuracy or precision for such complex issues.

Going back to the A68 report, yes, the static semantics is fully specified.
How? With a VERY hard to read program, almost comment free, written in a
very difficult to follow programming language (W grammars). Very precise,
but very inaccessible. Most people think that this approach was a mistake
in retrospect.

I personally liked the approach of the Ada 83 standard, which strived for
readability, while retaining a readsonable level of formality and
precision (I find the new Ada 95 standard far less successful in that
respect, since it deliberately abandoned the fierce emphasis on readability
in a quest for more formal precision -- the shift is not huge, but it is
noticeable, and aspects of the new Ada 95 standard are really quite difficult).

The PL/1 standard which you mention is indeed more formal, being inspired
by VDL, but again suffers in my view from an accessibility problem.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]