What are the semantics of your favourite programming language? | Hacker News Reader

What are the semantics of your favourite programming language?

plsadventures.com

17 pointsgdp20 comments

If you're wondering what things like "operational" and "denotational" mean and what they look like in code, I created this article for my compilers students:

http://matt.might.net/articles/writing-an-interpreter-substi...

Short version:

* A denotational semantics is a function M : Program -> (Value -> Value) that maps a program to a mathematical function.

* An operational semantics is a relation (=>) between consecutive machine states. That is, if state => state' holds, then the machine transitions from state to state'.

* The relation in a "big-step" operational semantics need not be decidable. Big-step relations are usually recursive.

* The relation in a "small-step" operational semantics must be decidable.

* When you implement a transition relation, =>, it's usually implemented as a function. That is, if you have a relation R \subseteq State x State, you can encode this as a "transfer function" f : State -> 2^State.

* Does the transfer function not need to take some input other than the state?

* Can you convert a denotational semantics to an operational semantics (and vice versa)? Is there any value in doing this?

* Does the transfer function not need to take some input other than the state?

It depends on how you're encoding things. You might want to supply the I in I/O as an extra parameter to the transfer function.

Or, you could kick off the execution with the state containing a (possibly infinite) sequence representing all of the I/O events it will encounter during execution.

For the most part, transfer functions operate on just states.

* Can you convert a denotational semantics to an operational semantics (and vice versa)? Is there any value in doing this?

Yes, Olivier Danvy has a strong research program in this area. He has a battery of techniques that allow you to (almost) mechanically calculate one kind of semantics from another.

In many cases, calculating an operational semantics from a denotational semantics is the easiest way to prove their equivalence.

Where is a good place to get started with studying formal semantics? I've tried to follow chapters about formal semantics in LiSP, TAPL, CTM, and _The Definition of Standard ML_ with varying degrees of success (the material in TDoSML was beyond me), but I'm not sure where to start. I know part of the issue is getting familiar with the dense notation. I'm gradually getting an intuition for the stuff, but reading the right book would go a long way.

I've wondered if this is one of the things I missed by being self-taught, but I don't think most programmers working in (say) Java or Python could really follow it either.

"Where is a good place to get started with studying formal semantics?"

I found "Design Concepts in Programming Languages" by Gifford and Turbak (http://www.amazon.com/Design-Concepts-Programming-Languages-...) well written and comprehensive. ( I am self taught too! :-))

I'll look into it, thanks!

Branching off the links that fadmmatt posted above, I found a booklist (http://matt.might.net/articles/books-papers-materials-for-gr...) with a PDF of Nielson & Nielson's Semantics with Applications (http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf). That looks good, too.

It sounds like I'm used to reading operational semantics, but have usually seen them specified in S-Expressions (as mini-interpreters in Scheme).

That's where a language's documentation intervenes. Some have a very small and simple core (Scheme) with well-defined behaviour.

Topic treated as well in the famous law of leaky abstractions : http://www.joelonsoftware.com/articles/LeakyAbstractions.htm...

I agree that documentation is useful and important, but too much programming languages documentation really doesn't answer some fundamental questions about the semantics of a language.

All too often, this is because the programming language designers/implementors don't know what the semantics are.

I'd say that having "a very small and simple core with well-defined behavior" is the exception, not the rule.

Off the top of my head, the only languages I can think of with small, precisely defined formal semantics are Scheme, SML, Joy, and Prolog.

You can add Lua to your list.

Here's the full manual including:

    - the language refenrence
    - all standard library functions
    - the C API.

TOC: http://www.lua.org/manual/5.1/

Manual: http://www.lua.org/manual/5.1/manual.html

It's very terse. The "Programming in Lua" book, by one of the authors of the language is far more friendly (an excellent book actually, the first version is available online for free: http://www.lua.org/pil/).

I use Lua quite a bit (Lua & C on Unix is my dev environment of choice, actually), but I haven't seen a written formal semantics for it, just the reference manual and bytecode guide. I'm thinking more like _The Definition of Standard ML_ - something that's very "math-y".

I was wondering about that today, actually - the designers are changing / simplifying the behavior for non-local environment scoping in Lua 5.2 (http://lua-users.org/lists/lua-l/2010-02/msg00753.html), and have been discussing the implications on the mailing list.

I follow that discussion too (and posted some messages). The new proposal is great IMO. Simple yet powerful.

There's no formal semantics, that's true, but I think one wouldn't be very long (although I would be absolutely unable to write it myself). The semantics of the more elaborate constructs of the language (the generic for loop, metamethods) are detailed in the manual as Lua code.

One could argue that code is math, according to the Curry-Howard isomorphism... But I'm no mathematician so I don't know if the point is valid in this context.

Would Erlang fit this catagory?

I ask because it's the language I'm trying to learn currently and so far it seems to have a core that's something like "Scheme with syntax" (Although I guess it's actually a lisp-2). But I don't know if it has weird edge cases that I haven't gotten to yet.

Erlang, too, has a core language which is pretty concise. I haven't seen a formal specification of its semantics, though.

FWIW, I found that Erlang made quite a bit more sense after I spent some time with Prolog. Erlang started out as a DSL built on SICStus Prolog, and a lot of its design decisions carried over from there.

The answers for the examples given near the end of the article are often present in language documentation. You can dig around and find the answer or you can spend two minutes and write a test or you can crash/debug later. In any case, you'll eventually find the answer.

The real issue is that programmers new to a language are unlikely to even realize there's a semantic boondoggle in a given situation. Had they read all of the documentation, perhaps they would - but that's obviously not what most people do. Adding more pages to the documentation just to collect all semantics in one place wouldn't seem to make it more likely that a new programmer is going to read and properly understand their implications.

I don't think you can solve the problem of inexperience with additional education, but it's a common idea in academic circles.

Arguably one of the reasons for the success of C was that it was introduced along with a comprehensive codebase- Unix- which made its semantics crystal clear.

It would be worthwhile to examine Github data to see how strong the correlation is between new languages and their adoption as a function of how large an initial codebase they come with.

blues.

greens?

orange you glad i didn't say yellows?

purpley not.

Reply on news.ycombinator.com