Reasoning about programs

Summary of last year

It has been quite a long time since my last post (which is also unfinished). Lots of things has happened and changed since last blog. I’ve been interning at Apple through the end of this summer. It was quite interesting and challenging at Apple, as I was supposed to support the team by developing monitoring and automation systems.

In another sense, the internship was a little bit boring. Tons of efforts were spent on trivial cases (such dealing with different formats of CSV files, or structure of HTML to extract information). Though the projects did include some interesting design, especially for the logic for concurrency: how the workers should update the database, how the worker share their credentials.

Both the interesting and the boring side of the internship make me long for advanced methods to deal with these kinds of stuff, which leads me to the field of formal verification.

Formal Verification

As a new comer to this field, I still may not figure out the exact meaning of it. But from my perspective, it’s all about reason about programs. “Formal” indicates that it is done through making specifications and using mathematical methods. Verification means to prove it working correctly.

Various methods were employed to reason about programs. (This list is limited due to my current knowledge, may be updated later).

Logic systems

Lots of systems were to assist proving programs. The most well-known one is the Hoare Logic, which is designed entirely based on the ALGOL 60 and works well in proving algorithms (In my opinion, the substitution rule for assignment is the greatest idea I’ve seen). Later other logic systems were also created based on Hoare’s work, such as separation logic.

SMT Solvers

SMT Solvers are not limited to the formal verification field, but they were quite useful. SMT solvers are helping us to proving things, especially those involved only with equations and inequalities(linear ones). Some verification-aware programming languages such as Dafny depend on these technologies(Z3). By the way, they are also the foundation of symbolic execution.

Type systems

Type systems might be rather simplified products of formal verification than things supports verification. This might be the most widely seen technology for common programmers. They were powerful in static analysis: With little expense(compared with other methods, such as proving specification about a program) but rather strong outcome.

What’s more

Although the name itself contains verification, but it certain possess greater potentials. Works have shown that it’s quite feasible to synthesize programs by reasoning about them. And I believe, this is where next computation revolution occurs.