<p>Formal semantics is useful primarily when you want to reason about programs. </p>

<p>In the past this was mainly done in programming language development (and to a lesser degree in compiler construction). Increasingly formal semantics is also used in automatic and interactive program verification, which is beginning to see industrial use. Since you are interested in compiler design, verified and certifying compilation is a hot research topic now that is based heavily on formal semantics. Check out the following systems.</p>

<ul>
<li><p>X. Leroy's <a href="http://compcert.inria.fr/">CompCert</a>. This was the first verified compiler: a realistic, moderately-optimizing compiler for a large subset of the C language down to PowerPC and ARM assembly code.</p></li>
<li><p>The MPI's <a href="http://plv.mpi-sws.org/pils/">Pilsner</a>, the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Most prior work (such as CompCert) has focused on verifying whole-program compilers. </p></li>
<li><p><a href="https://cakeml.org/">CakeML</a>. A compiler for an ML dialect. The focus of CakeML is on minimising the trusted computing base, not on optimisation or on breadth of source language features.</p></li>
<li><a href="http://arxiv.org/abs/1601.05520">Cogent</a>. A certified compiler from a simple functional language with linear types (useful for reasoning about memory management) to C.</li>
</ul>

<p>Progress on such compilers has been much swifter than many (including myself) anticipated, and I expect to see more and more of this work to seep into industrial compilers.</p>

<p>The problem with formal semantics is rarely to write down the semantics of a language. That's usually simple.  The real issue is how efficiently to prove theorems about programs in a language using the semantics. </p>

CC BY-SA 3.0
2016-02-16T12:53:31.167Z
2016-02-16T12:53:31.167Z
Martin Berger
<p>(If this is better for programmers SE, let me know, but I imagined you guys would have more thorough answers)</p>

<p>I'm a mathematics major, but I have a pretty deep interest in CS (especially in compiler design, reverse engineering, etc). </p>

<p><a href="http://www.msreverseengineering.com/program-analysis-reading-list/" rel="nofollow">This site</a> recommended <a href="http://rads.stackoverflow.com/amzn/click/1846286913" rel="nofollow">a book on formal semantics</a>. I imagine that a knowledge of semantics is useful there (but I'm not quite sure how, yet). Are there other fields in which this knowledge is directly useful, other than academic treatments of programming languages?</p>

<soft-question><pl.programming-languages><semantics>
In what fields does a knowledge of formal semantics prove useful?
galois
# In what fields does a knowledge of formal semantics prove useful?

(Asked by: username_0 on 2016-02-16)

(If this is better for programmers SE, let me know, but I imagined you guys would have more thorough answers)

I'm a mathematics major, but I have a pretty deep interest in CS (especially in compiler design, reverse engineering, etc).

[This site](http://www.msreverseengineering.com/program-analysis-reading-list/) recommended [a book on formal semantics](http://rads.stackoverflow.com/amzn/click/1846286913). I imagine that a knowledge of semantics is useful there (but I'm not quite sure how, yet). Are there other fields in which this knowledge is directly useful, other than academic treatments of programming languages?

**Tags:** soft-question, pl.programming-languages, semantics

---

## 1 answers

### Answer by username_1 on 2016-02-16. Score: 6

Formal semantics is useful primarily when you want to reason about programs.

In the past this was mainly done in programming language development (and to a lesser degree in compiler construction). Increasingly formal semantics is also used in automatic and interactive program verification, which is beginning to see industrial use. Since you are interested in compiler design, verified and certifying compilation is a hot research topic now that is based heavily on formal semantics. Check out the following systems.

* X. Leroy's [CompCert](http://compcert.inria.fr/). This was the first verified compiler: a realistic, moderately-optimizing compiler for a large subset of the C language down to PowerPC and ARM assembly code.
* The MPI's [Pilsner](http://plv.mpi-sws.org/pils/), the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Most prior work (such as CompCert) has focused on verifying whole-program compilers.
* [CakeML](https://cakeml.org/). A compiler for an ML dialect. The focus of CakeML is on minimising the trusted computing base, not on optimisation or on breadth of source language features.
* [Cogent](http://arxiv.org/abs/1601.05520). A certified compiler from a simple functional language with linear types (useful for reasoning about memory management) to C.

Progress on such compilers has been much swifter than many (including myself) anticipated, and I expect to see more and more of this work to seep into industrial compilers.

The problem with formal semantics is rarely to write down the semantics of a language. That's usually simple. The real issue is how efficiently to prove theorems about programs in a language using the semantics.


---

