What makes a good paper?

Or: Theorems are the test cases of semantics

Good PL papers define their systems with enough greek symbols, funky operators, inference rules and the like (what Mitch calls "dirty pictures") to demonstrate depth and precision of intellectual content. Without proving subsequent theorems based on these systems, though, there's no evidence that these systems are actually consistent or even useful.

A programming language semantics is, as Mitch puts it, "a mathematical model for predicting the behavior of physical systems." One of its primary purposes is reasoning (at a particular level of abstraction) about programs written in that language. It's generally hard to prove that a semantics is "the right one" for the problem space, which is a fuzzy notion, but theorems raise its probability of being useful.

A semantics alone may at least convey information about a language, since math is often more concise and precise than English. But without being put into use, it's doubtful whether it is really a specification; it's far too easy to slip into specifics as an algorithm. Or at the other extreme, it may leave out too many details to address the salient issues in the problem space. And who knows what subtle errors are lurking within the language definition? The best way to ensure that a semantics accurately defines a language at an appropriate level of abstraction is to prove theorems with it.