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.