2022-09-05

# λ. 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  . 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 logics 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.

1. Abstract stuff that is extracted from the concrete stuff.

PL Tools Distill