deductive proof nets

> I don't know whether emphasising so much computational complexity is the right 
> thing to do.
> [...] There is one thing that this complexity view doesn't require, namely the 
> kind of compositionality which is usually associated to deduction.

Compositionality seems central to me. While I would certainly expect 
that the task of verifying a proof is computationally easy, I think that 
I expect something more.

When I have to check a proof and in the middle of it I have to pop out 
for lunch then I can put a check mark on the lemmas that I've already 
checked such that when I come back I can resume where I left, without 
having to do anything twice. Of course there's a way to do the same 
thing with proof nets. But the question is: what does that mean, 
logically, to have checked half of the correctness criterion?

Shouldn't this be the difference between deductive, compositional (say 
sequent calculus) and non-deductive, global (say proof nets, connection 
method)? In the first case you do half of the work and you get some 
intermediate theorem from which the original theorem follows once you've 
done the other half. In the second case doing half the work doesn't get 
you that intermediate theorem, as far as I can see.

-Kai