Jan's reflections

The 1969 paper An Axiomatic Basis for Computer Programming by C.A.R. Hoare contains one of the first attempts at rigorous reasoning about computer programs. To date, the paper gathered over two thousand direct citations, and many software verification tools, both practical and academic, have been based on the ideas contained in the paper.

I am announcing Minuska: a truly formal programming language framework. One can use Minuska to specify programming language semantics - formally. From the semantics, Minuska can automatically derive a formally proven interpreter for the language. Minuska is formally specified, implemented, and proved using the Coq theorem prover, with a bit of OCaml used for its command-line interface.

A question:

In order to formally verify a piece of code, you need a formal specification. Then you need the code. Both the specification and the code describe the same thing - say, an algorithm. Of course, because otherwise the verification would fail. Therefore, formal verification requires describing one thing twice. How is that helpful? Especially if formal verification aims to reduce the amount of code one needs to trust…

TL;DR: If you find yourself coding a description of something twice, you are probably doing something wrong. Maybe you are writing the program, or the specification, in a wrong style. And maybe it is not your fault, because your languages do not allow you to do better.

Formal verification tools need to understand the programming language they target. For some of the tools, the understanding is represented implicitly in their code, while other are explicitly linked to a separate representation of the language. A tool in the latter category can also be created by semi-automatically deriving it from the language representation, as demonstrated by K-framework. In that case, the language is encoded explicitly in a formal semantics, the verification tool is built separately in a way that allows plugging in an arbitrary formal semantics, and then the two are combined. In this post I explore some advantages and limitations of this “language-parametric” approach.

In their CppCon'23 talk titled “Better Code: Contracts in C++”, Sean Parent and Dave Abrahams of Adobe advise developers on how to use a methodology known as “Design by Contract” to build better and safer systems. While the talk is targeted towards C++ developers, the methodology is fairly general and can be applied to other imperative languages as well. For me, the talk was really fun to watch, so I would definitelly recommend it to others. That said, I have a couple of remarks about the talk that I want to write down and share.

Recently I came across an interesting Empirical Software Engineering paper from 2013. In the paper, titled Bug characteristics in open source software, the authors reported on their studies of bugs in the Linux kernel, Mozilla (today known as Firefox), and the Apache server (all C/C++ projects at that time). They manually classified over 2000 bugs and, among other insights, found that around 2/3 of security vulnerabilities were caused by semantic bugs (which could be also labeled as “functional correctness” issues), compared to around 1/3 of vulnerabilities caused by memory bugs (buffer overflows, double frees etc). Moreover, the proportion of memory bugs was decreasing with time, as the projects were getting more mature. Does this mean that the efforts put into memory-safe languages like Rust are, so to speak, beating a dead bug?

Recently, a friend of mine asked me: “Do you think that all programming languages should have a formal semantics?”. I do not want to give a simple yes/no answer to that question. Instead, I would like to think about the value formal semantics provides and compare it with the alternatives programming languages have.