Re: Formal semantics of language semantics

Joe Hendrix wrote:
> Are there any notations commonly used to define the semantics of a
> programming language? (Similar to how BNF defines the syntax).


There are many notations, but none is common. Most have the problem
that expressing the semantics in them is longer than simply writing
down some code that "does the right thing". Those few notations that
don't have this problem are usually difficult to implement
efficiently.


And those that are both easy to write and efficiently implementable
are so near to being a programming language themselves that they tend
to become full programing languages almost naturally. The engine that
processes them is already a programming language interpreter, all you
need after that is adding a compiler, maybe a debugger, some libraries
that go beyond what's needed for programming language specification...


As a loosely related example, consider the ML family of languages.
Initially, there was a theorem prover, the language for specifying
theorems and proofs being ML. (I don't know whether that prover was
ever used to specify programming language semantics. It would have
been possible, because if you have a constructive proof that a
function exists, that proof can be automatically transformed into a
program that computes the function.)


Today, ML is the ancestor of two languages that are in near-production
use (SML and OCaml), and a plethora of research languages.


Regards,
Joachim

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