Yes, we finally jump to this volume which allows us to have a deeper understanding of modern programming languages!
This would cover:
When we are building a large system, it is common that bugs would appear in some very tricky way, and we want to eliminate such circumstances to a level that is acceptable for us all, but it is hard if we treat it as a technical issue: we write unit tests to check robustness of every single unit / module, which is tedious and often requires high amount of labor, and sometimes developers cannot cover all the possible cases (we often hear about a joke about testing a bar). Rather, we should treat the program as a precise, theoretical algorithm that can be models by mathematical languages. We can then prove the correctness of the program using mathematical reasoning, reducing the labor. The main tools for these tasks are abstract syntax and operational semantics, a method of specifying programming languages by writing abstract interpreters (check MIRAI for Rust verification). We will later develop the notion of Hoare Logic, a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs (ref. wikipedia).
Another thing is type system which is a powerful tool for establishing properties of all programs in a given programming language. Type systems are the best established and most popular example of a highly successful class of formal verification techniques known as lightweight formal methods.
$\lambda$-calculus is built upon these two key components.
(I thought there was no need to learn this chapter, but I was wrong… This chapter, in fact, contains a lot of necessary notions for me to proceed with the Hoare Logic.)
From here, let us mimic a small subset of common programming languages like Java or C.
We will present this language in three parts:
Inductive aexp : Type :=
| ANum (n : nat)
| APlus (a1 a2 : aexp)
| AMinus (a1 a2 : aexp)
| AMult (a1 a2 : aexp).
Inductive bexp : Type :=
| BTrue
| BFalse
| BEq (a1 a2 : aexp)
| BNeq (a1 a2 : aexp)
| BLe (a1 a2 : aexp)
| BGt (a1 a2 : aexp)
| BNot (b : bexp)
| BAnd (b1 b2 : bexp).
Next, we will need to evaluate an arithmetic expression, which finally produces a number. Similarly, evaluating a boolean expression yields a boolean.
Fixpoint aeval (a : aexp) : nat :=
match a with
| ANum n => n
| APlus a1 a2 => (aeval a1) + (aeval a2)
| AMinus a1 a2 => (aeval a1) - (aeval a2)
| AMult a1 a2 => (aeval a1) * (aeval a2)
end.
Fixpoint beval (b : bexp) : bool :=
match b with
| BTrue => true
| BFalse => false
| BEq a1 a2 => (aeval a1) =? (aeval a2)
| BNeq a1 a2 => negb ((aeval a1) =? (aeval a2))
| BLe a1 a2 => (aeval a1) <=? (aeval a2)
| BGt a1 a2 => negb ((aeval a1) <=? (aeval a2))
| BNot b1 => negb (beval b1)
| BAnd b1 b2 => andb (beval b1) (beval b2)
end.
Another way to think about evaluation is as a relation between expressions and their values, which is often more flexible. This leads naturally to Inductive definitions. It will be convenient to have an infix notation for aevalR. We'll write e ==> n to mean that arithmetic expression $e$ evaluates to value $n$.