8
$\begingroup$

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.

$\endgroup$
2
  • 2
    $\begingroup$ What is this question asking? Do you want to know how to formally define a programming language? $\endgroup$
    – Ginger
    May 16, 2023 at 17:34
  • $\begingroup$ Yes, updated; it's a broad question and might get some interesting answers I hope! $\endgroup$
    – Lee
    May 16, 2023 at 17:37

6 Answers 6

9
$\begingroup$

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:

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?
$\endgroup$
3
  • $\begingroup$ I love this answer; I wonder if a language's ground truth syntax and semantics must also include a description of the machine upon which the interpreted/compiled code runs? $\endgroup$
    – Lee
    May 17, 2023 at 8:47
  • 1
    $\begingroup$ Technically yes, but fortunately most machines run the exact same code with the exact same behavior (barring speed, which isn't considered behavior anyways) $\endgroup$
    – tarzh
    May 17, 2023 at 16:18
  • $\begingroup$ And factors like disk size, other files, etc. aren't considered part of the program's behavior $\endgroup$
    – tarzh
    May 17, 2023 at 16:19
9
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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.

$\endgroup$
3
  • 8
    $\begingroup$ A more recent (and more wide-spread) programming language with the same approach for specification is WebAssembly, which also has its typing and reduction defined in terms of inference rules, complemented with a reference interpreter and a formalizations in Isabelle and Coq. $\endgroup$ May 16, 2023 at 20:07
  • 1
    $\begingroup$ @MatijaPretnar Excellent, excellent! It's wonderful to hear about WebAssembly, I didn't know it was formalized to such degree. My focus has been on functional languages, like Standard ML, which sadly lack analogous modern results (besides CakeML) :( $\endgroup$ May 17, 2023 at 14:09
  • 1
    $\begingroup$ With regards to WebAssembly: they do some very interesting stuff around formal semantics, having a DSL for generating the typing rules, formal proofs, interpreter, and prose. $\endgroup$
    – apropos
    Sep 7, 2023 at 6:45
4
$\begingroup$

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
$\endgroup$
3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ While it's true that most languages don't have any formal communication, definition, or description, this doesn't seem to address the question of how one might do those things. $\endgroup$
    – Michael Homer
    Sep 6, 2023 at 7:04
  • $\begingroup$ @MichaelHomer I'd argue that you can always start by writing an interpreter ... That is in fact what I usually do. $\endgroup$ Sep 6, 2023 at 7:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .