Back to the email

That's the point I was trying to make: without explicitly listing your postconditions, users are free to infer whatever postconditions they want, making any kind of non-breaking change to the postconditions impossible. Every emacs update breaks someone's workflow, as they say!