# λ. Disclaim:

- This blog is a working draft and half-done (This sentence makes me relief).
- It’s too late today. I don’t run any spellcheck or even read it once.
- But it’s fine. A terrible-written blog follows the Matt’s blog tip: take it easy!

# λ. Main

Sometimes I am asked by other PhD students in the department on *how do PL people think about this question*, *how this topic is studies in PL*, *what is the PL persepective on this*. This is already the question on level 3. In the beginning, the question is usually (level 1) *what is PL* asked by enough many people, after I saying I am doing PL research. Then level 2 quesiton is what do you research. For this question, I strongly suggest Mike Hicks’s answer [1] [2]. The motivation between the level 3 question is usually people wants to bring more PL ideas and techniques in their own work. This post is for that question.

The core of PL is a set of *rules*. Sometimes we call it **logic**, or
we know it works like *logic* but we don’t say so. The other components are for making the logic run. We need to convert the system input into a format the *logic* can accept, what is usually done by a *parser*. We need an engine to *saturate* the logical rules and get the result.

In an interpreter, the **logic** is the operational semantics of the language. The **engine** is a recursive function `evaluate`

which takes each expression and find the matching rule in the logical system to apply. A common interpreter runs until it gets the final answer (or diverge). This is the **saturation** though each expression usually just be evaluated once.

In type inference, the **logic** is the typing rules. The **engine** is an algorithm to
compute the closure (fix-point) of type constraints on each expressions. The **saturation** means the compute is exhaustive with type informations. Static analysis is quite similar to this.

In symbolic execution, the **logic**s includes the operational semantics with constraints of the symbols and a SMT solver. What’s more, since a symbolic executor need to run all the possible control-flows at one forking point e.g. an if clause. How to deal with it will also be defined in the **logic**. In a nondeterministic setting (also called dynamic symbolic execution), the **logic** doesn’t need to change but the implemention need to handle the forking (or nondeterministic monad). If you need to apply state-merging, then how to merge should be defined in the **logic**.

In model checking, the **logic** is the abstract model, which can be e.g. some temporal logic in first-order model checking or HFL (higher order modal fixed point logic). You need to convert you program into this logical formula. To **saturate** it, run the model checking algorithm, or feed the formula into some solvers.

- Abstract stuff that is extracted from the concrete stuff.