Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
(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 recommended a book on formal semantics. 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?
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. 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, 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. 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.
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.
