• EarlyDays

Prehistory and Early Days

When understanding a subject it is helpful (and not emphasized enough in CS) to have a picture of the development of ideas.

Prehistory

An important precursor of separation logic is the following early paper in program logic.

• Some techniques for proving programs which alter data structures. RM Burstall. Machine Intelligence 7, 1972.

A key moment is when Burstall gives a proof of a list-reversal program, which he considers unacceptably tedious, and he says `instead we will try to do better'. Note that Burstall's system is theoretically adequate, and one could have probably proved a completeness theorem for it, etc, etc... but it wasn't good enough for him . Burstall then goes on to define "distinct non-repreating list systems" (dnrl's), which are not dissimilar to the specialized abstract domains used in heap analysis tools in the 2000s. He observes that computation steps which alter one component of a dnrl automatically leave the other components unchanged, and this short-circuits nasty aliasing problems that became problematic in subsequent proof techniques for pointers, allowing proofs to become considerably shorter.