The way I understand the difference is that ownership types constrain
the shape of the object graph, and substructural systems (like
separation logic) manage permissions to access the heap.
In the original work on ownership types, the idea is to maintain the
invariant of owners as dominators. An object $o$ is dominated by
an object $d$, if every path from the root set to $o$ contains $d$. So
$o$ is only reachable from $d$. So the system is designed so that
class declarations are parameterized by their owners, and then this
fact gives you a derived frame condition for $o$: its state cannot
change unless a method on its owner $d$ is invoked.
In contrast, substructural systems like linear types and separation
logic rely on the idea of resources. Each region of the heap is a
resource, and if you don't possess the resource you can't touch it.
This makes frame conditions very easy: they always hold.
One superficial difference (which nevertheless confused me for a long
time) was that ownership types were types, and separation logic was a
program logic. Luckily, while ownership types were born in a
type-theoretic setting, people have applied these ideas to program
logics as well.
The two main pieces of theoretical work I know on this are Kassios's
work on dynamic frames, which Bannerjee and Naumann (and their
students) systematically exploited in their work on regional logic.
As I understand it, their basic approach is to take Hoare logic, and
then:
- Add a new type of region variables, which you use to associate objects and regions.
- Add an effect system to Hoare logic to track the regions reads and writes touch.
- Use the effects to determine if an assertion is frame-respecting or not.
If it is, you can frame it, and if it isn't, you can't.
Each approach has benefits and weaknesses.
Ownership makes frame properties significantly less convenient to
use than in substructural approaches, since you have to compute frame
conditions.
On the other hand, algorithms on DAGs support prettier inductive
proofs in an ownership style, since you can decouple the footprint
from the pointer structure. In a separation-style spec, the natural
thing is to give an inductive invariant on a spanning tree. But if
the spanning tree the algorithm computes is ever different than the
one your invariant has, you're in for a world of hurt.
My general sense is that separation is easier to use than ownership,
since we need frame properties for nearly every command in an
imperative program. (Dave Naumann argues that region logic is more amenable to automation, since the assertion logic remains plain old FOL, and so
you can use off-the-shelf theorem provers and SMT solvers.)
EDIT: I just found the following paper by Matt Parkinson and Alex Summers, The Relationship between Separation Logic and Implicit Dynamic Frames, where they claim to give a logic unifying the two methods.