*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

Therefore, I start with the rule

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.

i know what you mean about separation logic not feeling much like a "logic", in the judgemental sense of the word.. i hear Neel has worked on various proof theoretic interpretations of separation logic -- maybe you should have a chat with him.

ReplyDeletebut yeah, i had the same feeling when i took the course, of not really knowing which rules to apply to get to where i needed to go, since all the rules just seemed kind of ad hoc.

> since all the rules just seemed kind of ad hoc.

ReplyDeleteMy feeling exactly.

Although I should point out that there were several times where I proved some program (albeit a small one) correct where the proof was very straightforward and seemed quite natural.