How might one formally communicate/define/describe a programming language design?

Question

How would one formally define a programming language?

What are the ways in which one can think about how to communicate a programming language design?

What languages and frameworks exist with which to define and describe programming languages?

Are there different layers of abstraction and/or categories to consider?

I've heard of K, which seems relevant and am wondering what alternatives there are and how they relate:

K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations and rules.

Answer 1

Generally, programming languages are modeled using specialized mathematical notation for humans, and/or in formal methods languages like K and also Coq and Redex for computers. An example of the human notation is on page 7 of Retrofitting Effect Handlers in OCaml, which defines the full operational semantics of multicore OCaml effect handlers. An example of the computer approach is in CompCert, a formally-verified C compiler: the team modeled the complete behavior of C and Assembly in Coq, including writing a C AST and assembly interpreter, and then the Coq proof checker used this model to prove that their compiler was behavior-preserving (the interpreted AST of any valid program has the same behavior as the compiled version).

Technically, a language's syntax and semantics are "defined" by its parser and interpreter/compiler, which is the ground truth, but there are many systems invented to better convey this information so it can be understood by humans and reasoned about by computers:

• Syntax: Via EBNF, ABNF, and other notations
• Semantics: Operational semantics (small-step and big-step), denotational semantics, evaluation strategy, typing rules, etc.

When describing a programming language and in particular its design, eventually you veer into informal territory. For example, usually syntactic sugar is completely invisible to the compiler, and certain constructs like do while loops, while loops, for loops, will be collapsed into a single representation (loops). These details aren't important for the formal definition (not very important to the computers), but some of them are very important to humans. Therefore, it's still best to describe some parts of your language informally in plain English, like:

• Is there a static or dynamic type system?
• Is memory management implicit or explicit?
• What's in its standard library?
• What are the coding conventions?
• How easy is the language to learn? Which languages will it be easier to transition from?

Answer 2

In conference papers, the usual way is:

• Extended BNF definition for the syntax, with textual description of some non-core features.
• Using inference rules (usually in the style of natural deduction) to describe the typing rules.
• Use induction on syntax or rewrite rules to define the operational semantics.

Example:

• Syntax: a, b, c ::= a + b | a > b | a ? b : c
• Textual description of non-core features: "we'll be using parentheses for precedences"
• Inference rules (one example):

  a : bool  b : τ  c : τ
  ----------------------
       (a ? b : c) : τ
  

• Operational semantics (one example):

  true ? b : c ---> b
  false ? b : c ---> c
  

The K framework provides a general framework for operational semantics with rewrite rules.

On the other hand, there is spoofax, which provides a datalog-style framework for typing rules.

Answer 3

There is the definition of Standard ML using operational semantics for its typechecking ("static semantics") and evaluation ("dynamic semantics"), which has been formalized with Twelf.

Answer 4

For completeness I must mention the C++ ISO standard.

While it doesn't include mathematic proofs like some answers. It does include:

• complete syntax
• very precise wording indicating how each language construct should behave whilst allowing for implementation specific / undefined behaviour.

Basically there are several compatible ways:

• syntax
• academic papers
• mathematical proofs relating to the type system and such like
• documentation thoroughly describing the language
• a reference implementation

Answer 5

What languages and frameworks exist with which to define and describe programming languages?

English is one such language.

Natural languages like English can absolutely be used for formal communication. The Java Language Specification is written in formal technical English, with a bit of mathematical notation mixed in where necessary.

For a taste, here's an excerpt from §15.12.2.5. Choosing the Most Specific Method: I've added bold formatting to highlight technical terms which are defined elsewhere in the JLS. (I've highlighted only the first use of each term.)

One applicable method $m_1$ is more specific than another applicable method $m_2$, for an invocation with argument expressions $e_1, \ldots, e_k$, if any of the following are true:

• $m_2$ is generic, and $m_1$ is inferred to be more specific than $m_2$ for argument expressions $e_1, \ldots, e_k$ by §18.5.4.

• $m_2$ is not generic, and $m_1$ and $m_2$ are applicable by strict or loose invocation, and where $m_1$ has formal parameter types $S_1, \ldots, S_n$ and $m_2$ has formal parameter types $T_1, \ldots, T_n$, the type $S_i$ is more specific than $T_i$ for argument $e_i$ for all $i$ ($1 \le i \le n$, $n = k$).

• $m_2$ is not generic, and $m_1$ and $m_2$ are applicable by variable arity invocation, and where the first $k$ variable arity parameter types of $m_1$ are $S_1, \ldots, S_k$ and the first $k$ variable arity parameter types of $m_2$ are $T_1, \ldots, T_k$, the type $S_i$ is more specific than $T_i$ for argument $e_i$ for all $i$ ($1 \le i \le k$). Additionally, if $m_2$ has $k+1$ parameters, then the $k+1$'th variable arity parameter type of $m_1$ is a subtype of the $k+1$'th variable arity parameter type of $m_2$.

It's very dense, but (as I've hopefully shown) every term used has a defined, specific meaning. Perhaps being in English, it is more likely to contain mistakes than if it were written in a formal language that could be verified; nonetheless, the JLS certainly communicates, defines and describes a programming language.

Answer 6

In practise, and despite most of the other answers, essentially the only way a mainstream, real world programming language $L$ is defined, is by building a $L$-compiler that translates to, or an $L$-interpreter that executes in another programming language (typically a machine language), which is assumed to be understood.

The others suggestion (like K, or natural deduction rules) are used for small toy languages, but not for mainstream, real world programming languages, such as C, C++, Haskell, Agda, Lean, Python etc. That's because the effort of fully defining the syntax and semantics of a mainstream PL is so heroic that one doesn't want to do it more than once. And where it is done more than once (e.g. clang and gcc) the results don't coincide ...

The reason why the other methods are used and very useful is essentially divide-and-conquer: we sketch the essence of computation mechanisms in toy calculi (e.g. $\lambda$-calculus for $\beta$-reduction, and $\pi$-calculus for message passing parallelism, or Datalog for proof search, ...), and ignore handling of various other problems (e.g. finiteness of numbers) because that would obscure the phenomenon we are trying to handle, and leave it to another toy model. The full, real-world compiler then 'only' has to solve of brining all those many different issues together in one unified whole. A good example here is ML, where Robin Milner separated out the presentation of type-inference into separate papers (e.g. L. Damas, R. Milner, Principal type-schemes for functional programs) which do not explain type inference for full ML, but only a toy model of it, a small λ-calculus. I think this is a good approach: compiler / interpreter + small calculi to exhibit novel ideas in the language.