Lambda the Ultimate

Nearly all languages with imperative elements have some kind of an array. In C
an array is just a typed pointer to a memory region. You can address the
different elements by giving an offset to the start of the memory region. The
compiler multiplies the offset with the size of the objects contained in the
array to get the actual offset in bytes.

The C view of arrays has certain advantages: It is memory efficient because it
uses just one pointer. Accessing elements is easy because it just needs some
simple address arithmetic.

But the C view has some pitfalls as well. First you might fail to allocate
memory for the array. Then the pointer to the memory region has some undefined
value. Second you might read elements of the array which have not yet been
initialized. Third you might read from or write to elements of the array which
are not within the allocated region.

Modern languages avoid this pitfalls by certain methods which can be executed
at compile time or at runtime. The failure to initialize the pointer to the
memory region is usually handled by initializing all pointers with zero. Any
access to a zero pointer results in a runtime exception. Addressing elements
outside the region is usually handled at runtime as well by storing with the
array its capacity and generating an exception if elements outside the region
are addressed.

All these solutions avoid memory corruption but they have a cost. Additional
code is required to check null pointer accesses and to check out of bound
accesses. The single pointer implementation is no longer sufficient because
the size of the allocated region has to be stored in the runtime object.

A language which allows formal verification can avoid all these pitfalls
without any cost. Without any cost? Well -- without any runtime and memory
footprint cost. But nothing is free. Some assertions must be provable at
compile time. I.e. whenever you want to access some element of the array you
have to be sure that the index is within the array bounds. And it is not
sufficient that you are sure. You have to convince the verifier of this fact.

In the article we show an array structure in our programming
language which allows us to convince the verifier that we make no illegal
accesses.

Since an array is a mutable structure we have to address the framing problem
as well. The framing problem is addressed appropriately if for any modifying
procedure it is clear not only what it does change but also what it leaves
unchanged.

A lot of effort is done currently in the verification community to address the
framing problem. Frame specifications like modify and use clauses for each
procedure, separation logic, different sophisticated heap models etc.

In the article we demonstrate that the framing problem can be solved without
all these complicated structures. It is sufficient to regard access to data
structures as functions and have a sufficient powerful function model. It is
amazing to see that proper abstraction makes some difficult seeming problems a
lot easier.

Around April 1 (but doesn't seem like a joke) 2013, on arxiv:
Alberto Carraro, Thomas Erhard, Antonino Salibra,
The stack calculus
(direct PDF link)

We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry–Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.

I haven't looked at the details yet, but the result are surprisingly simple and look deeply interesting -- if you're into that sort of thing. I was always a bit rebuted the relatively large size of classical calculi, with lots of rules on top of the lambda-calculus. This one doesn't have a lambda primitive (a bit like System L in this respect) and is surprisingly concise.

(Fun fact: intuitionistic calculi are structured by the fact that there is only one hypothesis on the right of the turnstile. They have at most one hypothesis on the left of the turnstile.)