Gagallium

This post discusses two ways of writing the Bind rule of Separation Logic. They are logically equivalent, but in practice, one should choose wisely between them.

In this post, I discuss two approaches to writing formal specifications for (possibly curried) functions of multiple arguments. I refer to these two styles as callee-side reasoning and caller-side reasoning. While the former style is very much standard, the latter style is perhaps relatively little known.