English
A programming language is a formal system for describing computations. The word “formal” does not mean stiff or academic; it means that the system has a precise definition — syntax rules that determine what counts as a valid program, and semantics that determine what that program does. The peculiar fact is that for most of computing’s history, this precision was largely absent. Languages were defined by their implementations, by reference manuals that were inconsistent, or by informal descriptions that different implementors read differently. Programming language theory is the discipline of replacing these informal definitions with mathematical ones, and reasoning about the consequences.
What makes the subject non-obvious is that “what a program means” is not a simple question. A program is a finite text; its execution is a process that may run for any duration, interact with an environment, allocate memory, raise exceptions, spawn threads, send network packets. The relationship between text and process is what semantics must specify, and specifying it precisely requires making choices: about what the observable behavior of a program is, about what counts as two programs being equivalent, about what properties you want to be able to prove. Programming language theory is organized around the tools for making these choices precisely and reasoning about their consequences.
The subject connects the computation axis at multiple points. Logic (§3.1) provides the proof-theoretic foundations — Hoare logic, type theory, and formal verification are all logical systems. Type theory (§3.5) is this subject taken to its deepest level: the study of what types are, what they can express, and their connection to mathematical proof. Formal methods (§3.6) applies the techniques developed here to the verification of real systems. Programming as conceptual practice (§2.1) is where these ideas connect to the activity of writing code; understanding one changes how you understand the other.
Prerequisites: Programming (§2.1) — you need fluency in at least one language to have concrete examples. Discrete mathematics (§2.2) — proof by induction is the primary proof technique. Logic (§3.1) — inference rules and formal systems are the medium the subject works in.
How Giving Meaning to Programs Became a Mathematical Discipline
The formal study of programming languages began not with programming but with logic. Alonzo Church invented the lambda calculus in the 1930s as a formal system for defining computable functions — one of the independent routes to the same destination as Turing machines. Lambda calculus, in its typed version, is the ancestor of every functional programming language and the mathematical foundation that programming language theory still uses as its primary object of study. Haskell Curry’s combinatory logic, developed in parallel, provided an alternative formulation. Both were tools for mathematical logic; neither was intended for programming. The connection came later, and when it came it was surprising.
When the first high-level programming languages appeared in the 1950s — FORTRAN in 1957, COBOL in 1959 — the question of what they meant was answered pragmatically: they meant what the compiler produced. Different compilers for the same language could behave differently, and the language had no authoritative definition beyond the reference manual, which was ambiguous on many points. ALGOL 60, designed by an international committee in 1960, was the first language for which formal definition was seriously attempted. Peter Naur’s Backus-Naur Form (BNF), introduced in the ALGOL 60 report, gave the syntax a rigorous grammar. But the semantics — the meaning of programs rather than their structure — was given only informally, in careful English prose, and different readers interpreted it differently.
The problem of formal semantics became urgent in the late 1960s when it became clear that informal descriptions were insufficient for proving programs correct, for compiling correctly, or for reasoning about program equivalence. Peter Landin’s work in the mid-1960s showed how to give ALGOL a precise semantics by translation into lambda calculus — an early connection between the logical tradition and the programming language tradition. Christopher Strachey, working at Oxford, developed denotational semantics alongside Dana Scott: instead of describing how a program executes (operational), denotational semantics describes what mathematical object a program denotes. A function in a programming language denotes a function in mathematics; a command in an imperative language denotes a state transformer — a function from program states to program states. Scott’s contribution was the domain theory that made this mathematically coherent: programs can loop, and a looping program should denote something (the “bottom” element of a semantic domain representing nontermination), and Scott showed how to build mathematical models where this was consistent.
The operational approach, given its definitive formulation by Gordon Plotkin in his 1981 “Structural Operational Semantics” lecture notes (widely circulated, formally published decades later), defined meaning by the computation steps a program takes — small-step operational semantics specifying each individual evaluation step, big-step (natural) semantics specifying the complete evaluation of an expression to its value. Plotkin’s formulation was precise enough to prove things about, flexible enough to handle a wide range of language features, and close enough to how programmers think about programs that it became the dominant style in programming language research papers.
Robin Milner’s work on ML in the early 1970s produced two contributions that changed the field. The first was the Hindley-Milner type inference algorithm (the name reflects independent prior work by Roger Hindley), which showed that types for a simply-typed program could be inferred from the program’s structure without any annotation by the programmer. This made the theoretical apparatus of typed lambda calculus usable in practice: a programmer could write code in the natural functional style, and the type checker would infer and verify the types automatically. The second was ML’s standard treatment as a formal object with a precise mathematical definition — Milner, Tofte, Harper, and MacQueen’s 1990 Definition of Standard ML is one of the rare examples of an industrial-strength programming language defined by a complete formal semantics, written in a mathematical style that supports rigorous reasoning.
John Reynolds’ 1983 paper “Types, Abstraction, and Parametric Polymorphism” established parametricity — the principle that a polymorphic function’s behavior is fully determined by its type. A function of type ∀α. α → α must be the identity function, because it has no way to inspect the type α. This gave a mathematical justification for the kind of “theorems for free” that Philip Wadler would later popularize: type signatures of polymorphic functions carry proofs of their properties as mathematical consequences, provable without examining the implementation. Reynolds also developed the foundational work on the semantics of imperative languages that would eventually become separation logic.
The 1980s and 1990s saw the framework mature into a research community with its own journals, conferences (POPL, founded 1973, became the flagship venue), and a stable set of problems. Type systems became more sophisticated — subtyping, intersection types, existential types, effect systems. The semantics of concurrency emerged as a major subfield with process calculi (Milner’s CCS and pi-calculus, Hoare’s CSP) providing the formal tools for reasoning about concurrent programs. The Curry-Howard correspondence, connecting types to logical propositions and programs to proofs, became the organizing intellectual theme — treated in full in §3.5.
The contemporary period has brought two significant shifts. The first is the movement of formal methods from proof-of-concept to industrial practice. Rust’s type system — with its ownership model encoding linear logic’s resource constraints — enforces memory safety without a garbage collector, a property formally proved for a core calculus. TypeScript, Kotlin, Swift, and Scala have brought sophisticated type systems to contexts where dynamic languages previously dominated. The influence of the theory on industrial language design has never been greater. The second shift is the emergence of proof assistants — Coq, Lean, Isabelle, Agda — as the medium in which programming language metatheory is increasingly conducted. The Software Foundations series, written entirely as Coq proofs, defines the standard treatment of programming language semantics; the POPLmark challenge in 2005 catalyzed the transition to mechanized metatheory by proposing a standard set of benchmark lemmas (proving the type preservation and progress theorems for System F) to be formalized in any proof assistant. The field now expects major semantic results to come with machine-checked proofs, a standard of rigor that is without precedent in computer science.
Meaning, Equivalence, and Type Soundness
The Four Traditions for Giving Meaning to Programs
Operational semantics defines meaning by the computation steps a program takes. Small-step operational semantics specifies each individual reduction step as an inference rule: from what syntactic forms, under what conditions, to what next form. Big-step (or natural) semantics specifies the complete evaluation of an expression to its value in a single judgment. Both styles use the same inference rule notation as logic (§3.1) — a horizontal line separating premises from conclusion, with the rule’s name at the right. The inference rules are the semantics: a program means the value (or sequence of values) to which these rules reduce it.
Operational semantics is the closest to how programmers think about programs — it describes what happens — and it is the most commonly used style in contemporary research. Its proofs tend to be syntactic, by induction on derivation trees. Its weakness is that it does not directly answer the equivalence question: two programs with different operational behavior might still be considered equivalent if their observable outputs agree.
Denotational semantics defines meaning by the mathematical object a program denotes. Each syntactic expression is mapped, by a compositional function ⟦·⟧, to a mathematical value: numbers to natural numbers, functions to set-theoretic (or domain-theoretic) functions, commands to state transformers. Denotational semantics supports equivalence reasoning directly: two programs are equivalent if and only if they denote the same object. It supports reasoning about infinite behavior — a looping program denotes the bottom element of a semantic domain — and supports a compositional theory of programming languages. Its weakness is the mathematical machinery: domain theory, the solution of recursive domain equations, and the full apparatus of denotational semantics requires significant mathematical background.
Axiomatic semantics (Hoare logic and its descendants) defines meaning by what programs guarantee about their pre- and post-conditions. A Hoare triple {P} C {Q} states that if predicate P holds before command C executes, and C terminates, then predicate Q holds after. The rules of Hoare logic combine these triples compositionally: the rule for sequential composition says that if {P} C₁ {Q} and {Q} C₂ {R} then {P} C₁; C₂ {R}. Axiomatic semantics is the natural framework for program verification and for the specification of software behavior. It supports automated reasoning through the weakest precondition calculus: given a postcondition Q and a command C, the weakest precondition wp(C, Q) is the most general predicate that, if it holds before C, guarantees Q after.
Separation logic, developed by John Reynolds, Samin Ishtiaq, and Peter O’Hearn in the early 2000s, extends Hoare logic with the separating conjunction P * Q — which asserts that P and Q hold for disjoint parts of the heap. This single extension makes it possible to reason about pointer programs locally: a specification says what a function does to its own part of the heap and nothing else, without mentioning the rest of the heap at all. Separation logic is the framework in which Rust’s ownership model can be formally understood: ownership is the proof that you have exclusive access to a piece of memory, which is the separating conjunction at work.
Behavioral equivalence — contextual equivalence, observational equivalence, bisimulation — asks when two programs are the same for practical purposes. The standard definition: two programs P and Q are contextually equivalent if no context — a program with a hole — can distinguish them by their observable outputs. This is the “real” equivalence for a programming language, because it captures what a user (or a compiler) can observe. Bisimulation, used in process calculi, is a coinductive notion of equivalence that works for infinite processes: two processes are bisimilar if they can always match each other’s observable transitions. Proving bisimulation equivalences requires different techniques than proving Hoare triples, and both are part of the practitioner’s toolkit.
Type Systems and Soundness
A type system is a syntactic discipline that classifies expressions by type and uses those types to rule out certain programs before they are run. The primary purpose is safety: a type-safe program cannot encounter certain runtime errors, where “certain runtime errors” depends on the type system’s design.
The canonical definition of type soundness, due to Andrew Wright and Matthias Felleisen (1994), uses two properties: progress (a well-typed program that is not a value can take a step — it is not stuck) and preservation (if a well-typed expression takes a step, the result is also well-typed). Together, these establish that well-typed programs cannot reach stuck states — states where the program tries to perform an operation that is ill-defined, like applying an integer as a function. The proof technique, “progress and preservation,” is called the syntactic soundness proof and is the standard method for proving type systems correct.
Type inference — automatically determining types without annotation — was the central practical advance that made typed languages usable. Hindley-Milner type inference computes the most general type (the principal type) for any expression in the simply-typed lambda calculus with let-polymorphism, in polynomial time. This makes it possible to write Haskell or OCaml or ML programs without type annotations and have the type checker infer and verify the types automatically. Extensions to Hindley-Milner — higher-kinded types, type classes, GADTs — are studied in contemporary type system research.
Parametric polymorphism (generics) allows code to work over multiple types. A function ∀α. α → α is parametric in α: it works for any type, and by Reynolds’ parametricity theorem, it must be the identity. This is “theorems for free”: the type signature of a polymorphic function entails behavioral properties of the function, without examining its implementation. The free theorems are not always interesting, but when they are — for example, that map f . map g = map (f . g) follows from the type of map — they eliminate large classes of program bugs as logical impossibilities.
Dependent types allow types to depend on values: the type of “a list of length n” where n is an ordinary runtime value. This expressive power allows specifications to be embedded directly in types — “a sort function that returns a sorted permutation of its input” can be expressed as a type — and the type checker’s verification of the type is a proof of the specification. Dependent types are the foundation of proof assistants like Coq, Lean, and Agda, and increasingly of production languages like Idris and the experimental features of Haskell. The price is that type checking becomes undecidable for sufficiently expressive dependent types, requiring annotations or restricted fragments.
Operational Techniques: Big Steps and Small Steps
The choice between small-step and big-step operational semantics is not aesthetic; it affects what properties are easy to prove and what the semantics can express.
Small-step semantics defines a reduction relation → where e → e’ means “expression e reduces to e’ in one step.” A computation is a sequence e₀ → e₁ → e₂ → … terminating at a value or diverging. Small-step semantics handles nontermination naturally (divergence is an infinite reduction sequence) and supports coinductive reasoning. It is the natural setting for the progress-and-preservation proof of type soundness.
Big-step semantics defines an evaluation relation ⇓ where e ⇓ v means “expression e evaluates to value v.” Big-step semantics is closer to the implementation — a big-step rule for function application directly describes how the function is called and the result returned. But big-step semantics handles nontermination awkwardly: a diverging expression simply has no evaluation judgment, and distinguishing “diverges” from “stuck” requires additional structure.
Evaluation contexts — a syntactic notation for identifying the “current focus” of computation — make small-step semantics more concise. The reduction rules apply to redexes (reducible expressions), and evaluation contexts specify where in a larger expression the next redex is. This decomposition supports the systematic study of reduction strategies (call-by-value, call-by-name, call-by-need) and their interaction with type systems and effects.
What Studying This Changes
Programming language theory changes what a practitioner can see in a programming language and in a program.
The first change is the ability to read a language specification rather than a language implementation. A practitioner without this training understands a programming language by accumulating examples, reading the manual, and consulting the implementation when the manual is ambiguous. A practitioner with formal semantics training can read the inference rules that define the semantics and derive consequences directly. This makes specifications the authoritative source rather than a secondary document that practitioners consult as a last resort.
The second change is structural recognition across languages. Every language with lexical scoping, structured control flow, and algebraic data types is, at the semantic level, a variant of the typed lambda calculus. Recognizing this makes learning new languages much faster — not because the surface syntax is similar, but because the underlying semantic structures are familiar. Rust’s ownership is linear type theory. TypeScript’s structural typing is the same subtyping relation Winskel describes. Python’s duck typing is an informally implemented form of nominal and structural equivalence. The practitioner who has studied the semantic theory sees these connections; the practitioner who has only used the languages does not.
The third change is type system intuition. Type systems are often experienced as an external constraint: a set of rules the compiler enforces, sometimes helpfully, sometimes frustratingly. After studying type theory, they become a specification language: a way of encoding properties that programs should have, with the type checker as an automatic verifier. This reframing changes how types are used. Instead of writing code and then satisfying the type checker, the practitioner designs types first, uses them to capture invariants, and lets the type checker enforce them.
The fourth change is access to the formal verification tools that the field has produced. Proof assistants — Coq, Lean, Isabelle, Agda — require understanding the type-theoretic foundations to use beyond the tutorial level. The formal verification of real software (the CompCert verified C compiler, the seL4 verified operating system kernel, the Rust formalization) is conducted using the techniques that programming language theory developed. A practitioner who has studied the formal semantics understands what these tools are doing and can use them to verify their own software.
Resources
Books and Texts
Pierce’s Types and Programming Languages (TAPL, MIT Press, 2002) is the canonical entry point and has been for over twenty years. It develops the typed lambda calculi systematically — simply typed lambda calculus, subtyping, recursive types, universal and existential polymorphism, higher-kinded types — with complete proofs of type soundness for each system. The book is demanding but pedagogically generous: every definition is accompanied by examples, every theorem is proved, and the exercises build genuine competence. For readers coming to PLT from a CS background with discrete mathematics and proof experience, TAPL is the right starting point. Pierce’s companion volume, Advanced Topics in Types and Programming Languages (ATTAPL, MIT Press, 2005), extends into advanced topics: dependent types, effect systems, typed assembly language, distributed programming.
Harper’s Practical Foundations for Programming Languages (PFPL, 2nd ed., Cambridge, 2016, draft free online) covers broader ground than TAPL — it includes imperative features, concurrency, and a more complete treatment of advanced type theory — but with denser writing. PFPL is organized around “abstract binding trees,” a formalism for reasoning about syntax with binding that is more general than the presentations in TAPL. Readers willing to invest in the denser presentation get a more complete and contemporary picture of the field.
Winskel’s The Formal Semantics of Programming Languages (MIT Press, 1993) is the classical treatment of operational and denotational semantics with less emphasis on type systems. If TAPL is the type-theorist’s bible, Winskel is the semanticist’s. It covers structural operational semantics, natural semantics, domain theory, and denotational semantics with mathematical precision. For readers who want the semantic perspective rather than the type-systems perspective, Winskel is the right primary text.
Friedman and Wand’s Essentials of Programming Languages (EOPL, 3rd ed., MIT Press, 2008) approaches the material through implementation: readers build interpreters for languages of increasing complexity, and the type systems and semantic concepts are introduced in the context of working implementations. EOPL is more accessible to readers who find the formal texts too abstract initially, and it makes the connection between theory and implementation explicit. For readers who struggle with TAPL’s pace, EOPL first then TAPL is a productive route.
Krishnamurthi’s Programming Languages: Application and Interpretation (PLAI, free online; optional paid print) is another implementation-first route, using interpreters and language variation to make semantic ideas concrete. It is less mathematically deep than TAPL and PFPL, but it is one of the best bridges for programmers who need to build languages before they can comfortably prove things about them.
Reynolds’ Theories of Programming Languages (Cambridge, 1998) develops the semantics of both functional and imperative languages from a categorical perspective and is the right text for readers who want the denotational and axiomatic semantics in depth, including the foundations of separation logic.
For proof assistant-based programming language theory, Pierce et al.’s Software Foundations series (free at softwarefoundations.cis.upenn.edu) is essential. Volume 1 (Logical Foundations) teaches Coq while introducing logic and proof; Volume 2 (Programming Language Foundations) formalizes operational semantics, type systems, and Hoare logic in Coq. The series is the standard treatment of PLT in mechanized form and is increasingly required reading for anyone who intends to do formal verification work.
For process calculi and concurrent languages, Milner’s Communicating and Mobile Systems: the Pi-Calculus (Cambridge, 1999) is the primary source for the pi-calculus, and Sangiorgi and Walker’s The Pi-Calculus: A Theory of Mobile Processes (Cambridge, 2001) is the comprehensive reference.
| Book | Role | Type |
|---|---|---|
| Pierce, Types and Programming Languages (TAPL) | Canonical entry; type systems | Entry |
| Pierce (ed.), Advanced Topics in Types and Programming Languages (ATTAPL) | Extension of TAPL | Depth |
| Harper, Practical Foundations for Programming Languages (PFPL, draft free) | Broader comprehensive alternative | Depth |
| Winskel, The Formal Semantics of Programming Languages | Operational and denotational semantics | Depth |
| Friedman & Wand, Essentials of Programming Languages (EOPL) | Implementation-first accessible entry | Practice |
| Krishnamurthi, PLAI (free; optional paid print) | Implementation-first PL concepts | Entry |
| Reynolds, Theories of Programming Languages | Denotational + axiomatic at depth | Depth |
| Pierce et al., Software Foundations Vols. 1–2 (free) | Mechanized PLT in Coq | Practice |
| Milner, Communicating and Mobile Systems | Pi-calculus primary source | Depth |
Courses and Lectures
Penn CIS 500 (Software Foundations, Benjamin Pierce, free materials) is the course that TAPL was written for. Complete lecture slides and supplementary materials are freely available. Pierce’s teaching integrates the formal material with programming exercises, and the course structure reveals the pedagogical approach behind the textbook.
Carnegie Mellon 15-312 (Principles of Programming Languages, Robert Harper, free materials) uses PFPL and is Harper’s primary teaching vehicle. His lecture notes develop the material with characteristic directness and are worth reading alongside or instead of PFPL for specific topics.
Oregon Programming Languages Summer School (OPLSS), held annually in Eugene, archives all lectures freely on YouTube. OPLSS attracts leading researchers and the lecture series covers topics from introductory PLT through the research frontier. Specific lecture series to prioritize: Frank Pfenning on proof theory and type theory; Andrew Pitts on nominal techniques; Paul-André Melliès on linear logic and game semantics.
Software Foundations exercises in Coq, available at softwarefoundations.cis.upenn.edu, constitute a self-paced course that develops mechanized proof skills alongside PLT content. Working through Volume 2 produces both PLT knowledge and Coq competence simultaneously.
| Course | Platform | Type |
|---|---|---|
| Penn CIS 500 Software Foundations (Pierce, free) | Penn course site | Entry |
| CMU 15-312 Principles of PL (Harper, free) | CMU course site | Depth |
| OPLSS lectures (free) | YouTube / OPLSS site | Reference |
| Software Foundations exercises in Coq (free) | softwarefoundations.cis.upenn.edu | Practice |
Practice, Tools, and Current Sources
Working through inference rules by hand — deriving small-step reduction sequences, constructing type derivations — is the primary cognitive work of learning PLT, and there is no substitute for it. For every language system in TAPL or PFPL, writing out the inference rules on paper and deriving several examples builds the operational intuition that reading cannot.
PLT Redex (Racket library, free) provides an environment for defining and testing operational semantics by running reduction rules on example programs. It is the tool Pierce designed to make TAPL’s formalism executable. For every language in TAPL, implementing it in Redex and running the test cases makes the formal definitions live.
Andrej Bauer and Matija Pretnar’s Programming Languages Zoo (free) is a collection of miniature languages demonstrating parsing, interpreters, compilers, static and dynamic typing, subtyping, polymorphism, lazy evaluation, exceptions, and abstract machines. It is especially useful after a reader has learned the concepts and wants to see compact implementations side by side.
Coq / Lean 4 / Agda — working through PLT results in a proof assistant is the highest-quality engagement with the material. The Software Foundations series in Coq is the primary structured path. Any proof-assistant formalization of type soundness (progress and preservation) produces a deep understanding of what the formal claims actually are that a pen-and-paper proof does not always provide.
The POPLmark Challenge (poplmark.org) proposed benchmark proofs for PLT metatheory in 2005; the solutions in various proof assistants are freely available and serve as worked examples of mechanized PLT.
| Resource | Platform | Type |
|---|---|---|
| PLT Redex (free) | Racket / racket-lang.org | Practice |
| Programming Languages Zoo (free) | plzoo.andrej.com | Practice |
| Software Foundations in Coq (free) | softwarefoundations.cis.upenn.edu | Practice |
| POPLmark challenge solutions (free) | poplmark.org | Practice |
| Lean 4 / Mathlib PLT formalizations (free) | leanprover-community.github.io | Reference |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| The notation barrier stops learners before the content begins | Inference rules, semantic brackets, judgment forms, and meta-variable conventions are dense and unfamiliar. Learners who encounter inference rules for the first time in TAPL sometimes conclude the subject is inaccessible and stop. The notation is a foreign language — fluency comes from use, not from understanding the grammar before reading. | Read TAPL’s first three chapters slowly and repeatedly, working through every inference rule by hand. After five or six complete derivation examples, the notation becomes natural. The investment is ten hours; the return is access to the entire subject. Stopping at the notation barrier foregoes the content for a temporary discomfort. |
| Treating semantics as optional for “real” programmers | The most capable practitioners in Rust, Haskell, or any language with a sophisticated type system rely constantly on semantic intuitions — about type safety, about ownership, about the behavior of abstractions at the boundaries where documentation runs out. These intuitions are either grounded in formal semantics or they are guesses. Groundless intuitions about type-theoretic behavior are a reliable source of subtle bugs. | Study the formal semantics of at least one language you use in practice. For Rust practitioners: read the formalization of ownership in terms of linear types and separation logic. For Haskell practitioners: work through the Hindley-Milner algorithm. The formal understanding does not replace practical experience; it gives it a foundation. |
| Confusing language implementation with language theory | Building a tree-walking interpreter for a toy language teaches parsing, evaluation, and the difficulties of implementation. It does not teach formal semantics, type soundness, or the abstract properties of language features. The two activities are related but distinct. Learners who do one and expect to have done the other will be confused by the discrepancy. | Treat language implementation and language theory as complementary skills that should both be developed. Use PLT Redex to run formal semantics, and use a separate implementation project (EOPL, or a compiler course) to build an interpreter. Both inform each other, but neither substitutes for the other. |
| Staying only in the typed functional setting | Most PLT resources — TAPL, PFPL, EOPL, the POPL community — use typed functional languages as the primary object of study. This is pedagogically reasonable but produces practitioners who are comfortable with pure functional semantics and uncomfortable with imperative languages, concurrency, and effects. Most deployed software is imperative and concurrent. | After acquiring the typed functional foundation, explicitly study the semantics of the languages you use in practice. Read about separation logic for C-like languages, session types for concurrent protocols, effect systems for languages like Scala or Koka. The foundation transfers; the application requires deliberate extension. |
| Skipping mechanized proofs as “just formalization” | Pen-and-paper proofs in PLT research papers regularly contain errors — small gaps in inductive cases, missing lemmas, implicit assumptions. Machine-checked proofs are the standard in high-quality PLT research because they eliminate these errors. A learner who has never formalized a type soundness proof in Coq or Lean has not experienced the full discipline that mechanized PLT requires. | Work through at least the type soundness proofs in Volume 2 of Software Foundations. The experience of having Coq reject a proof that looks correct on paper — because a case is missing, or a lemma is applied in the wrong direction — is one of the most educational experiences the subject offers. |
| Learning only type systems without learning semantics | TAPL’s emphasis on type systems can create the impression that type theory is the whole of programming language theory. Operational semantics, denotational semantics, program equivalence, bisimulation, and concurrency theory are equally fundamental and are poorly represented in TAPL. The practitioner who knows only type systems lacks the tools for reasoning about program equivalence, for specifying concurrent behavior, or for understanding what “the semantics of Python” even means. | Use Winskel as a counterweight to TAPL. After working through TAPL’s type systems, read Winskel’s operational and denotational semantics chapters. The semantic perspective — what programs mean rather than what types they have — is the foundation that type theory is built on, and it deserves direct study. |
中文
编程语言是一种用于描述计算的形式系统。“形式”并不意味着僵硬或学院化；它意味着这个系统有精确定义——语法规则决定什么算作合法程序，语义决定这个程序做什么。奇特的是，在计算的大部分历史中，这种精确性基本缺席。语言由其实现来定义，由彼此不一致的参考手册来定义，或由不同实现者会作出不同理解的非形式描述来定义。编程语言理论，就是用数学定义替代这些非形式定义，并推理其后果的学科。
这个主题不显然的地方在于，“一个程序是什么意思”并不是一个简单问题。程序是一段有限文本；它的执行则是一个过程，可能运行任意长时间，与环境交互，分配内存，抛出异常，生成线程，发送网络包。文本与过程之间的关系，正是语义必须规定的东西；而要精确规定这种关系，就必须做出选择：关于程序的可观察行为是什么，关于两个程序在什么意义上等价，关于你想要证明哪些性质。编程语言理论围绕一组工具组织起来，用来精确做出这些选择，并推理其后果。
这个主题在多个点上连接计算轴。逻辑（§3.1）提供证明论基础——Hoare logic、类型论和形式验证都是逻辑系统。类型论（§3.5）是本主题推进到最深处的形态：研究类型是什么、类型能表达什么，以及它们与数学证明之间的联系。形式化方法（§3.6）把这里发展出的技术应用于真实系统的验证。作为概念实践的编程（§2.1）则是这些思想与写代码活动相连接的地方；理解其中一者，会改变你对另一者的理解。
前置知识：编程（§2.1）——你需要熟练掌握至少一门语言，才能拥有具体例子。离散数学（§2.2）——归纳证明是主要证明技术。逻辑（§3.1）——推理规则和形式系统是本主题工作的媒介。
给程序赋予意义如何成为一门数学学科
对编程语言的形式研究并非始于编程，而是始于逻辑。Alonzo Church 在 1930 年代发明 λ 演算，作为定义可计算函数的形式系统——这是通向与图灵机相同目的地的几条独立道路之一。λ 演算的类型化版本，是所有函数式编程语言的祖先，也是编程语言理论至今仍作为主要研究对象的数学基础。Haskell Curry 并行发展出的组合逻辑，则提供了另一种表述。二者本来都是数理逻辑工具；都不是为了编程而设计的。联系是后来才出现的，而且当它出现时，令人意外。
1950 年代第一批高级编程语言出现时——1957 年的 FORTRAN，1959 年的 COBOL——“它们是什么意思”这个问题得到的是实践性回答：它们的意思就是编译器生成的东西。同一语言的不同编译器可以表现不同，而除了参考手册之外，语言并没有权威定义；参考手册在许多地方又是含糊的。ALGOL 60 由国际委员会在 1960 年设计，是第一门被认真尝试形式定义的语言。Peter Naur 在 ALGOL 60 报告中引入的 Backus-Naur Form（BNF），为语法提供了严格文法。但语义——程序的意义，而不是程序结构——仍然只是用谨慎的英文散文非形式地给出，不同读者会作出不同解释。
形式语义问题在 1960 年代末变得紧迫，因为人们清楚地看到，非形式描述不足以证明程序正确性，不足以正确编译，也不足以推理程序等价性。Peter Landin 在 1960 年代中期的工作展示了如何通过翻译到 λ 演算，为 ALGOL 提供精确语义——这是逻辑传统与编程语言传统之间的早期连接。Christopher Strachey 在 Oxford 工作期间，与 Dana Scott 一起发展了指称语义：它不是描述程序如何执行（操作式），而是描述程序指称什么数学对象。编程语言中的函数指称数学中的函数；命令式语言中的命令指称状态转换器——也就是从程序状态到程序状态的函数。Scott 的贡献是 domain theory，它使这一切在数学上连贯：程序可能循环，而循环程序也应该指称某个东西，即语义域中表示不终止的 “bottom” 元素；Scott 展示了如何构造使这种处理一致的数学模型。
操作语义路径由 Gordon Plotkin 在 1981 年的 “Structural Operational Semantics” 讲义中给出决定性表述。这份讲义被广泛流传，几十年后才正式出版。操作语义通过程序所采取的计算步骤来定义意义——小步操作语义规定每一个单独求值步骤，大步（自然）语义规定一个表达式到其值的完整求值。Plotkin 的表述足够精确，可以用于证明；足够灵活，可以处理广泛语言特性；又足够接近程序员关于程序的思考方式，因此成为编程语言研究论文中的主导风格。
Robin Milner 在 1970 年代初关于 ML 的工作产生了两项改变领域的贡献。第一项是 Hindley-Milner 类型推断算法（名称反映了 Roger Hindley 更早的独立工作），它表明简单类型程序的类型可以从程序结构中推断出来，而不需要程序员添加任何标注。这使类型化 λ 演算的理论装置在实践中变得可用：程序员可以用自然的函数式风格写代码，而类型检查器会自动推断并验证类型。第二项是把 ML 标准地处理为一个具有精确数学定义的形式对象——Milner、Tofte、Harper 和 MacQueen 1990 年的 Definition of Standard ML，是少数工业强度编程语言由完整形式语义定义的例子之一，并以支持严格推理的数学风格写成。
John Reynolds 1983 年的论文 “Types, Abstraction, and Parametric Polymorphism” 确立了参数性——即多态函数的行为完全由其类型决定的原则。类型为 ∀α. α → α 的函数必然是恒等函数，因为它没有办法检查类型 α。这为 Philip Wadler 后来推广的 “theorems for free” 提供了数学正当性：多态函数的类型签名携带了关于函数性质的证明，这些性质作为数学后果成立，不需要检查实现。Reynolds 还发展了命令式语言语义的基础工作，后来成为 separation logic 的来源。
1980 年代和 1990 年代，这个框架成熟为一个拥有自身期刊、会议（POPL 创办于 1973 年，后来成为旗舰会议）和稳定问题集的研究共同体。类型系统变得更复杂——子类型、交类型、存在类型、效应系统。并发语义成为主要子领域，进程演算（Milner 的 CCS 和 pi-calculus、Hoare 的 CSP）为并发程序推理提供形式工具。Curry-Howard 对应把类型连接到逻辑命题、把程序连接到证明，并成为组织性的智识主题——§3.5 会完整处理这一点。
当代时期带来了两个重要转变。第一，是形式化方法从概念验证走向工业实践。Rust 的类型系统——其所有权模型编码了线性逻辑中的资源约束——在没有垃圾回收器的情况下强制内存安全，而这一性质已经在核心演算中得到形式证明。TypeScript、Kotlin、Swift 和 Scala 把复杂类型系统带入了此前由动态语言主导的语境。理论对工业语言设计的影响从未如此之大。第二个转变，是证明助手——Coq、Lean、Isabelle、Agda——成为越来越多编程语言元理论工作的媒介。完全以 Coq 证明写成的 Software Foundations 系列，定义了编程语言语义的标准处理方式；2005 年的 POPLmark challenge 则通过提出一组标准基准引理（证明 System F 的类型保持和进展定理，并要求在任意证明助手中形式化）催化了机制化元理论的转向。如今，这个领域期待重要语义结果配有机器检查证明；这种严格标准在计算机科学中没有先例。
意义、等价性与类型可靠性
给程序赋予意义的四种传统
操作语义通过程序所采取的计算步骤来定义意义。小步操作语义把每一个单独归约步骤规定为推理规则：从什么句法形式出发，在什么条件下，进入什么下一个形式。大步语义，或自然语义，则用一个单一判断规定一个表达式完整求值到其值。两种风格都使用与逻辑（§3.1）相同的推理规则记号——一条横线把前提与结论分开，规则名称写在右侧。推理规则就是语义：一个程序的意义，就是这些规则把它归约到的值，或值序列。
操作语义最接近程序员对程序的思考方式——它描述发生了什么——也是当代研究中最常用的风格。它的证明往往是句法性的，通过对推导树做归纳完成。它的弱点在于，它并不直接回答等价性问题：两个操作行为不同的程序，如果其可观察输出一致，仍然可能被认为是等价的。
指称语义通过程序所指称的数学对象来定义意义。每个句法表达式都会被一个组合式函数 ⟦·⟧ 映射到一个数学值：数字映射到自然数，函数映射到集合论函数或 domain-theoretic 函数，命令映射到状态转换器。指称语义直接支持等价性推理：两个程序等价，当且仅当它们指称同一个对象。它支持对无限行为进行推理——循环程序指称语义域中的 bottom 元素——并支持编程语言的组合式理论。它的弱点是数学机器：domain theory、递归域方程的求解，以及完整指称语义装置，都要求相当数学背景。
公理语义（Hoare logic 及其后继者）通过程序对前置条件和后置条件作出什么保证来定义意义。Hoare 三元组 {P} C {Q} 表示：如果命令 C 执行前谓词 P 成立，并且 C 终止，那么执行后谓词 Q 成立。Hoare logic 的规则会组合这些三元组：顺序组合规则说，如果 {P} C₁ {Q} 且 {Q} C₂ {R}，那么 {P} C₁; C₂ {R}。公理语义是程序验证和软件行为规约的自然框架。它通过最弱前置条件演算支持自动推理：给定后置条件 Q 和命令 C，最弱前置条件 wp(C, Q) 是最一般的谓词，只要它在 C 之前成立，就能保证 C 之后 Q 成立。
Separation logic 由 John Reynolds、Samin Ishtiaq 和 Peter O’Hearn 在 2000 年代初发展出来，它用 separating conjunction P * Q 扩展 Hoare logic——该连接词断言 P 和 Q 分别在堆的 不相交 部分上成立。这个单一扩展，使局部推理指针程序成为可能：规约只说一个函数会如何处理自己那部分堆，而完全不提堆的其余部分。Separation logic 是形式理解 Rust 所有权模型的框架：所有权就是你拥有某块内存独占访问权的证明，而这正是 separating conjunction 在起作用。
行为等价性——上下文等价、观察等价、bisimulation——询问两个程序什么时候在实践意义上是相同的。标准定义是：如果没有任何上下文——也就是一个带洞的程序——能够通过可观察输出区分程序 P 和 Q，那么 P 和 Q 是上下文等价的。这是编程语言的“真实”等价性，因为它捕捉了用户或编译器能够观察到的东西。Bisimulation 用于进程演算，是一种适用于无限过程的共归纳等价概念：如果两个进程总能匹配彼此的可观察转换，那么它们就是 bisimilar。证明 bisimulation 等价所需技术不同于证明 Hoare 三元组；二者都是实践者工具箱的一部分。
类型系统与可靠性
类型系统是一种句法纪律，它按类型分类表达式，并利用这些类型在程序运行前排除某些程序。其主要目的在于安全性：一个类型安全程序不会遇到某些运行时错误；而“某些运行时错误”具体指什么，取决于类型系统的设计。
由 Andrew Wright 和 Matthias Felleisen（1994）给出的类型可靠性经典定义使用两个性质：进展（一个良类型程序如果不是值，就可以继续迈出一步——它不会卡住）和 保持（如果一个良类型表达式迈出一步，其结果仍然良类型）。二者合在一起确立了：良类型程序不会到达卡住状态——也就是程序试图执行没有定义的操作，例如把整数当作函数应用。这个证明技术，即 “progress and preservation”，被称为句法可靠性证明，是证明类型系统正确性的标准方法。
类型推断——无需标注就自动确定类型——是使类型化语言可用的核心实践进展。Hindley-Milner 类型推断可以在带 let-polymorphism 的简单类型 λ 演算中，为任意表达式以多项式时间计算出 最一般 类型，即 principal type。这使人在编写 Haskell、OCaml 或 ML 程序时，可以不写类型标注，而由类型检查器自动推断并验证类型。Hindley-Milner 的扩展——高阶类型、type classes、GADTs——都是当代类型系统研究对象。
参数多态，也就是 generics，允许代码作用于多个类型。函数 ∀α. α → α 对 α 是参数性的：它适用于任何类型，并且根据 Reynolds 的参数性定理，它必然是恒等函数。这就是 “theorems for free”：多态函数的类型签名蕴含了该函数的行为性质，无需检查实现。当这些 free theorem 有意义时——例如 map f . map g = map (f . g) 可以从 map 的类型推出——它们会把大量程序 bug 排除为逻辑不可能。
依赖类型允许类型依赖值：例如“长度为 n 的列表”这个类型，其中 n 是普通运行时值。这种表达力允许把规约直接嵌入类型中——“一个排序函数返回输入的有序排列”可以被表达为类型——而类型检查器对该类型的验证，就是对规约的证明。依赖类型是 Coq、Lean 和 Agda 等证明助手的基础，也越来越多出现在 Idris 这样的生产语言，以及 Haskell 的实验性特性中。代价在于，足够有表达力的依赖类型会使类型检查不可判定，因此需要标注或受限片段。
操作技术：大步与小步
在小步和大步操作语义之间选择，并不是审美问题；它会影响哪些性质容易证明，以及语义能够表达什么。
小步语义定义一个归约关系 →，其中 e → e’ 表示“表达式 e 在一步中归约为 e’”。一次计算是一个序列 e₀ → e₁ → e₂ → …，最终终止于一个值，或发散。小步语义自然处理不终止情况，因为发散就是无限归约序列，并且支持共归纳推理。它是类型可靠性的进展—保持证明的自然场景。
大步语义定义一个求值关系 ⇓，其中 e ⇓ v 表示“表达式 e 求值为值 v”。大步语义更接近实现——函数应用的大步规则会直接描述函数如何被调用以及结果如何返回。但大步语义处理不终止时比较笨拙：一个发散表达式只是没有求值判断；要区分“发散”和“卡住”，就需要额外结构。
求值上下文是一种用于识别计算“当前焦点”的句法记号，可以使小步语义更简洁。归约规则作用于 redex，也就是可归约表达式；而求值上下文指定这个 redex 位于更大表达式中的哪里。这种分解支持系统研究归约策略——call-by-value、call-by-name、call-by-need——以及它们与类型系统和效应之间的相互作用。
学习这个主题会改变什么
编程语言理论会改变实践者在编程语言和程序中能够看见的东西。
第一种变化，是能够阅读语言规约，而不只是阅读语言实现。没有这种训练的实践者，通过积累例子、阅读手册，并在手册含糊时查实现，来理解一门编程语言。受过形式语义训练的实践者，则能够阅读定义语义的推理规则，并直接推导后果。这使规约成为权威来源，而不是实践者最后才求助的次级文档。
第二种变化，是跨语言的结构识别。任何拥有词法作用域、结构化控制流和代数数据类型的语言，在语义层面上都是类型化 λ 演算的变体。识别这一点，会使学习新语言变快——不是因为表层语法相似，而是因为底层语义结构熟悉。Rust 的所有权是线性类型论。TypeScript 的结构化类型是 Winskel 所描述的同一种子类型关系。Python 的 duck typing 是名义等价和结构等价的一种非形式实现。学习过语义理论的实践者能看见这些连接；只使用过这些语言的实践者则看不见。
第三种变化，是类型系统直觉。类型系统常被体验为一种外部约束：一套由编译器执行的规则，有时有帮助，有时令人沮丧。学习类型论之后，它们会变成一种规约语言：一种编码程序应当具有的性质的方式，而类型检查器则是自动验证器。这种重构会改变类型的使用方式。实践者不再先写代码再满足类型检查器，而是先设计类型，用类型捕捉不变量，并让类型检查器强制它们成立。
第四种变化，是进入这个领域所产生的形式验证工具。证明助手——Coq、Lean、Isabelle、Agda——如果要在教程层级之外使用，就需要理解其类型论基础。真实软件的形式验证，例如 CompCert 验证 C 编译器、seL4 验证操作系统内核、Rust 形式化，都是用编程语言理论发展出的技术完成的。学习过形式语义的实践者，会理解这些工具在做什么，并能用它们验证自己的软件。
资源
书籍与文本
Pierce 的 Types and Programming Languages（TAPL，MIT Press，2002）是经典入口，二十多年来一直如此。它系统发展类型化 λ 演算——简单类型 λ 演算、子类型、递归类型、全称与存在多态、高阶类型——并为每个系统给出完整的类型可靠性证明。这本书要求较高，但在教学上很慷慨：每个定义都有例子，每个定理都有证明，习题会建立真正能力。对于具备 CS 背景、离散数学和证明经验后进入 PLT 的读者，TAPL 是正确起点。Pierce 的配套卷 Advanced Topics in Types and Programming Languages（ATTAPL，MIT Press，2005）则延伸到高级主题：依赖类型、效应系统、类型化汇编语言、分布式编程。
Harper 的 Practical Foundations for Programming Languages（PFPL，第 2 版，Cambridge，2016，网上有免费草稿）覆盖面比 TAPL 更广——包括命令式特性、并发，以及对高级类型论更完整的处理——但写作更密集。PFPL 围绕 “abstract binding trees” 组织，这是一种用于推理带绑定语法的形式系统，比 TAPL 中的呈现方式更一般。愿意投入阅读这种密集表达的读者，会获得更完整、更当代的领域图景。
Winskel 的 The Formal Semantics of Programming Languages（MIT Press，1993）是操作语义和指称语义的经典处理，对类型系统的强调较少。如果 TAPL 是类型理论家的圣经，那么 Winskel 就是语义学家的圣经。它以数学精确性覆盖结构化操作语义、自然语义、domain theory 和指称语义。对于想获得语义视角，而不是类型系统视角的读者，Winskel 是正确主文本。
Friedman 和 Wand 的 Essentials of Programming Languages（EOPL，第 3 版，MIT Press，2008）通过实现进入材料：读者会为复杂度逐步上升的语言构建解释器，而类型系统和语义概念则在工作实现的语境中被引入。对于一开始觉得形式文本过于抽象的读者，EOPL 更容易进入，并且明确展示理论与实现之间的连接。对 TAPL 节奏感到吃力的读者，先读 EOPL 再读 TAPL 是一条有效路线。
Krishnamurthi 的 Programming Languages: Application and Interpretation（PLAI，在线免费；可选付费纸质版）是另一条实现优先路线，通过解释器和语言变体使语义思想具体化。它没有 TAPL 和 PFPL 那样深的数学深度，但对需要先构建语言、再舒服地证明语言性质的程序员来说，是最好的桥梁之一。
Reynolds 的 Theories of Programming Languages（Cambridge，1998）从范畴视角发展函数式和命令式语言的语义，是想深入学习指称语义和公理语义，包括 separation logic 基础的读者应读的文本。
对于 基于证明助手的编程语言理论，Pierce 等人的 Software Foundations 系列（softwarefoundations.cis.upenn.edu 免费）是必要资源。第一卷 Logical Foundations 在教授逻辑和证明的同时教授 Coq；第二卷 Programming Language Foundations 在 Coq 中形式化操作语义、类型系统和 Hoare logic。这个系列是机制化形式下 PLT 的标准处理，也越来越成为任何计划做形式验证工作的人必须阅读的内容。
对于 进程演算和并发语言，Milner 的 Communicating and Mobile Systems: the Pi-Calculus（Cambridge，1999）是 pi-calculus 的主要来源；Sangiorgi 和 Walker 的 The Pi-Calculus: A Theory of Mobile Processes（Cambridge，2001）则是综合参考。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Pierce，Types and Programming Languages（TAPL） | 经典入口；类型系统 | 入门 |
| Pierce 编，Advanced Topics in Types and Programming Languages（ATTAPL） | TAPL 的延伸 | 深入 |
| Harper，Practical Foundations for Programming Languages（PFPL，草稿免费） | 更广泛的综合替代文本 | 深入 |
| Winskel，The Formal Semantics of Programming Languages | 操作语义与指称语义 | 深入 |
| Friedman & Wand，Essentials of Programming Languages（EOPL） | 实现优先的易进入入口 | 实践 |
| Krishnamurthi，PLAI（免费；可选付费纸质版） | 实现优先的 PL 概念 | 入门 |
| Reynolds，Theories of Programming Languages | 指称语义 + 公理语义深入处理 | 深入 |
| Pierce 等，Software Foundations Vols. 1–2（免费） | Coq 中的机制化 PLT | 实践 |
| Milner，Communicating and Mobile Systems | Pi-calculus 一手来源 | 深入 |
课程与讲座
Penn CIS 500（Software Foundations，Benjamin Pierce，免费材料）是 TAPL 最初对应的课程。完整讲义 slides 和补充材料都可以免费获取。Pierce 的教学把形式材料与编程练习结合起来，而课程结构也显示了教材背后的教学方法。
Carnegie Mellon 15-312（Principles of Programming Languages，Robert Harper，免费材料）使用 PFPL，是 Harper 的主要教学载体。他的讲义以其一贯的直接风格展开材料，针对具体主题，可以与 PFPL 一起读，或替代 PFPL 阅读。
Oregon Programming Languages Summer School（OPLSS） 每年在 Eugene 举办，并在 YouTube 免费存档全部讲座。OPLSS 吸引一线研究者，讲座系列覆盖从入门 PLT 到研究前沿的主题。优先推荐的具体系列：Frank Pfenning 关于证明论和类型论；Andrew Pitts 关于 nominal techniques；Paul-André Melliès 关于线性逻辑和 game semantics。
Software Foundations 的 Coq 练习，可在 softwarefoundations.cis.upenn.edu 获取，构成一门自定节奏课程，在发展 PLT 内容的同时发展机制化证明能力。完成第二卷会同时获得 PLT 知识和 Coq 能力。
| 课程 | 平台 | 类型 |
|---|---|---|
| Penn CIS 500 Software Foundations（Pierce，免费） | Penn 课程网站 | 入门 |
| CMU 15-312 Principles of PL（Harper，免费） | CMU 课程网站 | 深入 |
| OPLSS 讲座（免费） | YouTube / OPLSS 网站 | 参考 |
| Software Foundations 的 Coq 练习（免费） | softwarefoundations.cis.upenn.edu | 实践 |
实践、工具与当前来源
手工推导推理规则——写出小步归约序列、构造类型推导——是学习 PLT 的主要认知工作，没有替代品。对于 TAPL 或 PFPL 中的每个语言系统，把推理规则写在纸上，并推导几个例子，会建立阅读无法产生的操作直觉。
PLT Redex（Racket 库，免费）提供了一个定义和测试操作语义的环境，可以在示例程序上运行归约规则。它是 Pierce 为了让 TAPL 的形式系统可执行而设计的工具。对于 TAPL 中的每一种语言，用 Redex 实现它并运行测试案例，会让形式定义活起来。
Andrej Bauer 和 Matija Pretnar 的 Programming Languages Zoo（免费）是一组微型语言集合，展示解析、解释器、编译器、静态和动态类型、子类型、多态、惰性求值、异常和抽象机。它尤其适合读者已经学过概念之后，用来并排查看紧凑实现。
Coq / Lean 4 / Agda——在证明助手中完成 PLT 结果，是与材料发生最高质量接触的方式。Coq 中的 Software Foundations 系列是主要结构化路径。任何关于类型可靠性（进展和保持）的证明助手形式化，都会让人深入理解这些形式主张究竟是什么；这是纸笔证明不总能提供的。
POPLmark Challenge（poplmark.org）在 2005 年为 PLT 元理论提出了一组基准证明；各种证明助手中的解法都可以免费获得，是机制化 PLT 的 worked examples。
| 资源 | 平台 | 类型 |
|---|---|---|
| PLT Redex（免费） | Racket / racket-lang.org | 实践 |
| Programming Languages Zoo（免费） | plzoo.andrej.com | 实践 |
| Software Foundations in Coq（免费） | softwarefoundations.cis.upenn.edu | 实践 |
| POPLmark challenge solutions（免费） | poplmark.org | 实践 |
| Lean 4 / Mathlib PLT formalizations（免费） | leanprover-community.github.io | 参考 |
陷阱
| 陷阱 | 为什么会误导 | 更好的回应 |
|---|---|---|
| 记号障碍让学习者在内容开始前停下 | 推理规则、语义括号、判断形式和元变量约定密集且陌生。学习者第一次在 TAPL 中遇到推理规则时，有时会断定这个主题无法进入，然后停下。记号是一门外语——流利度来自使用，而不是在阅读前先完全理解语法。 | 慢慢、反复阅读 TAPL 前三章，手工推导每一条推理规则。完成五六个完整推导例子之后，记号会变得自然。投入大约十小时；回报是进入整个主题。停在记号障碍处，就是因为暂时不适而放弃真正内容。 |
| 把语义看作“真正”程序员可有可无的东西 | Rust、Haskell 或任何具有复杂类型系统语言中的最强实践者，都持续依赖语义直觉——关于类型安全，关于所有权，关于抽象在文档无法覆盖边界处的行为。这些直觉要么建立在形式语义上，要么只是猜测。没有根基的类型理论行为直觉，是细微 bug 的可靠来源。 | 至少学习一门自己实际使用语言的形式语义。Rust 实践者：阅读从线性类型和 separation logic 角度对所有权的形式化。Haskell 实践者：推导 Hindley-Milner 算法。形式理解不会替代实践经验；它会给实践经验提供基础。 |
| 混淆语言实现与语言理论 | 为玩具语言构建 tree-walking interpreter，会教授解析、求值和实现困难。它不会教授形式语义、类型可靠性或语言特性的抽象性质。这两项活动相关，但不同。做了其中一项，就以为自己完成了另一项的学习者，会被二者之间的差异弄糊涂。 | 把语言实现和语言理论看作互补能力，二者都应发展。用 PLT Redex 运行形式语义，再用单独实现项目（EOPL 或编译器课程）构建解释器。二者彼此提供信息，但谁也不能替代谁。 |
| 只停留在类型化函数式设定中 | 多数 PLT 资源——TAPL、PFPL、EOPL、POPL 共同体——都以类型化函数式语言为主要研究对象。这在教学上合理，但会培养出熟悉纯函数式语义、却不熟悉命令式语言、并发和效应的实践者。大多数已部署软件是命令式且并发的。 | 获得类型化函数式基础之后，要明确学习自己实践中使用语言的语义。阅读类 C 语言的 separation logic、并发协议的 session types、Scala 或 Koka 等语言中的 effect systems。基础可以迁移；应用需要有意识延伸。 |
| 把机制化证明当作“只是形式化”而跳过 | PLT 研究论文中的纸笔证明经常包含错误——归纳情形中的小缺口、缺失引理、隐含假设。机器检查证明成为高质量 PLT 研究标准，正是因为它能消除这些错误。一个从未在 Coq 或 Lean 中形式化类型可靠性证明的学习者，还没有经历机制化 PLT 所要求的完整纪律。 | 至少完成 Software Foundations 第二卷中的类型可靠性证明。让 Coq 拒绝一个纸面上看似正确的证明——因为少了一个情形，或一个引理用反了方向——是这个主题能提供的最有教育意义的体验之一。 |
| 只学类型系统，不学语义 | TAPL 对类型系统的强调，可能让人以为类型论就是整个编程语言理论。操作语义、指称语义、程序等价、bisimulation 和并发理论同样基础，而在 TAPL 中呈现不足。只懂类型系统的实践者，缺少推理程序等价、规定并发行为，或理解“Python 的语义”究竟意味着什么所需的工具。 | 用 Winskel 平衡 TAPL。完成 TAPL 的类型系统之后，阅读 Winskel 的操作语义和指称语义章节。语义视角——程序 意味着什么，而不是程序 具有什么类型——是类型论建立其上的基础，也值得直接学习。 |