Separation logic began as a treatment of programs which worked on independent areas of the store. We've now found how to describe and reason about sharing, ownership transfer and concurrency primitives like semaphores and conditional critical regions. We think we have a new take on critical sections, which we can treat formally.

There are problems which we are still struggling with: there seems to be more than one model, matching more than one kind of sharing/separation; we haven't quite conquered sharing and ownership of variables; we haven't mechanised our logic. Nevertheless, we think we have punched a very big hole in the walls of the problem of safe concurrent programming through which we can drive quite a lot of logical tanks.

The overall purpose of this work is to facilitate resourcing, a step beyond typing which will allow static analysis of programs to ensure they don't overstep their resource bounds. It's a Grand Challenge for formalists, the next big step forward in our mission to make programming more reliable.

For those who like proof theory and exciting speculation, I'll give a glimpse of a possible treatment of variables-as-resource.