1. 14
  1. 7

    Separation logic is marketed as something for theoreticians: it’s a family of program logics to formally prove things about programs using resources (possibly concurrently). But my experience is that it is also hugely useful for the practice of programming, it gives a series of tools to think about concurrent programs using mutable state – my favorite is the presentation of locks as owning invariants, whose ownership is temporarily transferred to the code fragments taking the lock. I find it much easier to think about my concurrent code using these reasoning tools than without. I think all programmers writing concurrent code with explicit critical sections should read up on concurrent separation logic.