Comment by nicksdjohnson

I don't think I follow - why would you need to reason about your callers' internal states in order to prove properties about your own contract?