Re: Formal semantics of language semantics

> I found Benjamin Pierce's new book "Types and Programming Languages"
> be an excellent introduction to specifying and using semantics, as
> well as on types. It's aimed at a fairly low reading level, so that
> you don't need a math degree to understand it.


I agree, Benjamin Pierce's book is really good. I took a course on
Type Theory and the instructure used a draft of the book. It was
pretty smooth. However I don't agree that the material is trivial.
True that you don't need a math degree but should know basic set
theory and logic (proof by induction, proof by contradiction etc.).
Basically, you should know discreet math. That is the only prereq to
understand the book.




> I have no idea how well the methods in the book scale to larger, more
> complicated programming languages. In industry, everyone seems to use
> natural language most of the time. Then, if they really want a formal
> sematics, then they may write one up in a theorem prover such as HOL.
> These after-the-fact semantics are almost certainly horrendous to
> read, though I admit I haven't even bothered to try. It's interesting
> to consider what it wold be like if languages were formally specified
> from the beginning.


These methods have been used to define most part of Java (and some
problems in its type system were discovered in the process). If you
are interested you can take a look of a paper in ACM's TOPLAS:
        http://portal.acm.org/citation.cfm?doid=503502.503505
or http://www.cis.upenn.edu/~bcpierce/papers/fj-tr.ps
This paper is by Atsushi Igarashi, Benjamin Pierce, Philip Wadler.
There are papers from other authors as well, some of them are:
        http://research.microsoft.com/~dsyme/reports/java.ps
        http://www-sop.inria.fr/oasis/personnel/Marjorie.Russo/java/
There are more, but I have to dig.


I think nobody in the industry uses formal semantics because of two
reasons:


1. most of the formal semantics papers/books start with defining
      a notation and then build a type system framework on top of it.
      So, unlike BNF, there are multiple notations out there, and a
      symbol in two notations might mean two different things. notations
      are converging but still there are gaps. I think that over time,
      some notation might become a de facto standard notation to describe
      type systems. Perhaps, someone will write a handbook to use for
      reading and defining type systems.


2. formal semantics is not as easy as formal syntax, simply because
      semantic rules are much more complex than syntax rules. It is very
      hard to read and understand formal semantics of a non trivial
      language. If you look at complete set of formal semantics rules
      for a language with basic OO features (inheritence, method
      overloading and overriding), I bet anybody would be scared. It
      takes time, effort and persistence to become confortable with it.
      Once you are confortable, you might happen to like it because these
      rules are very precise. I think that is why people settled for
      ambiguous prose describing semantic rules.


+satish

Return to the comp.compilers page.
Search the comp.compilers archives again.