Correctness by design vs. formal verification

One common debate in the programming language community is the notion of correctness by design vs. verifying the correctness of your program. After all, if you can guarantee that all the programs that you write to be correct by construction, then there is no need to separately prove its correctness (using program analysis, formal verification, you name it), which is arguably non-trivial in general. How might you ensure correctness by construction? One easy way is to design a programming language that *rules out* certain bugs. For example, back in the 2001 when I started learning programming in C and then C++, I had to learn how to debug segmentation faults. A switch to higher-level programming languages like Java and Python ensures that I don't have to deal with segmentation faults anymore (assuming the correctness of JVM and Python interpreters). Can you do the same with other kinds of errors?

An interesting CACM article that I recently read (https://cacm.acm.org/magazines/2017/5/216322-ending-null-pointer-crashes/fulltext) discusses how the programming language Eiffel eliminates the problem of null pointer crashes (which could cause serious security vulnerabilities). A null pointer dereferencing happens when you invoke x.f in an object-oriented programming language, where x is a variable pointing to null and f is a field. It turns out that eliminating null pointer dereferencing by language design in a way that does not severely limit the expressiveness and convenience of the language is not straightforward, as discussed in the article. Eiffel instead relies on sophisticated use of type checking and static analysis to ensure that a program that passes an Eiffel compiler cannot exhibit null pointer crashes. So, the case study of Eiffel seems to suggest that correctness should be achieved not only by only language design or software verification alone, but by both of them simultaneously.

What about other kinds of programming errors, e.g., cross-site scripting in HTML5, data race condition in concurrent programming?

When does Bob deserve to be a co-author?

I have recently been reading Bill Gasarch's post about when Alice deserves to be a co-author. This is definitely a sensitive issue; just check the number of ANONYMOUS comments. I have recently found some advice that is more oriented towards faculty-student type of collaborations, but is perhaps also suitable in general. Check this link. Interestingly, it was a document written by Department of City and Regional Planning, University of Berkeley ...

Highland workshop on XML, Logic, and Automata

I'll be attending Highlands Workshop on XML, Logic, and Automata organized by Leonid from tomorrow until this Sunday. The venue is actually quite interesting: a small town in the Highlands called Grantown-on-spey. I'm just hoping that they have a grocery store :) I will give a presentation on recurrent reachability in regular model checking based on this paper. Anyway, I'll post a summary of the workshop later on this week.

Rahul Santhanam has joined Edinburgh

Rahul Santhanam, Lance Fortnow's ex PhD student, has recently joined Edinburgh's School of Informatics. Warm welcome to him!

Finite-variable hierarchy conjecture

It seems that Ben Rossman has resolved another long-standing open problem in finite model theory: finite-variable hierarchy conjecture. Loosely speaking, the conjecture is that over ordered graphs first-order logic with k+1 variable is more powerful than first-order logic with k variable. The problem is nicely summarized in Anuj Dawar's survey. Ben has shown that this hierarchy is strict. What was previously known is that (over ordered graphs) first-order logic with 3 variables is strictly more expressive than first-order logic with 2 variables, but it was not known whether first-order logic with 3 variables is less expressive than first-order logic with k variables, for every k > 3. Worse yet, it wasn't even known whether this hierarchy is strict. See Anuj Dawar's survey for further details.

I believe this is the third big open problems that Ben has resolved in this decade. Go Ben!