> it implies an often unrealistic separation between writing specs and writing implementations

I think that part of the problem is that small modification in the spec can lead to enormous changes in the proofs