## Monday, March 2, 2009

### Separation Logic

Today was the last day of "Introduction to Separation Logic," a mini-course that I am taking from the creator of Separation Logic himself, John C. Reynolds. It was a good course. Even though I found it difficult, I actually got a quite a good deal out of the course because I decided to take it for credit and therefore I actually did the homework. This will come as no surprise to many of you, but if you actually do the assignments in a course that is centered around proofs you get so much more out of it than if you kind of just take the theorems as already having been proved by someone else.

The weird thing about separation logic (for me) is how different it is from other logics that I have learned which were based upon "hypothetical reasoning." Hypothetical reasoning, I am lead to believe, it pretty much the latest, greatest way of presenting a logic. You get this context of assumptions and then you can do your reasoning from there, using facts from your context whenever necessary.

Proofs in Separation Logic had a much different feel. In it, you have a whole bunch of rules that are implications. There also aren't really introduction and ellimination rules, just more rules. Every single proof that I did was like this:
I want to prove
P => D

P => P

Then I find things that P implies that are slighly closer to D...
P => P'

and I have to use the rule, "P=>Q and Q => R means P => R" at every step along the way... Not sure if that makes sense, but it was new for me.

If you're interested, and outside of CMU, you can get the lecture notes for the entire course from John's web site. This is a great way to learn separation logic which has recently become kind of a big deal.