Programming Languages and Local Reasoning

Through time, there have been two interesting trends in programming languages: towards better guarantees and later binding.

With "guarantees", I mean facts and invariants which the language rules permit us to conclude from the code. Such as the following - you may or may not recognize them (and the language features which give rise to them):

• "The value in this variable is of this type."
• "The value in this variable can only come from one of these expressions."
• "The value of this object field can not be changed once the object has been constructed."
• "This variable can only be accessed from one thread."
• "This method can not be redefined in subclasses."
• "This process will always be notified when this other process disappears."
• "If this code point is reached, then this other code point will eventually be reached."

The two trends, better guarantees and later binding, correspond to two desirable properties of software: the ability to reason about the behaviour of software, and flexibility.

Introduction

About me:

I have a background in theoretical computer science (Master's degree from University of Aarhus). I currently work as a software developer (developing in Erlang, Scala, and the odd Bash, Perl and C++).

I've been involved - briefly - in many software projects; as bug reporter, coder, translator, or level designer. You could call me a hit-and-run contributor.
The reason: I tend to have too many ideas of my own to explore to hang around any particular project for long. Perhaps not ideal, but that's how it's turned out.

My main interests are programming languages and their implementations. That means primarily compilers, but also interpreters and runtime systems.