Dynamic Logic: The good parts

A while ago I'd bought a book on Dynamic Logic on a whim. I came to know of the existence of such a field through a dismissive comment from Spolsky (or was it Yegge?) and apparently thought it worth my money to see if it was indeed to be dismissed thusly.

The book lay unread in my book case in India for a few years until my wife brought it by mistake to Chicago, where it again lay unread. Finally as I returned to India, I put the book in the "throw/drop into building library" pile, but just couldn't do it because it was after all a book.

So while my favorite books took the slow way home via ship, this book that I didn't really care much for travelled with me and became my reading material for the initial days in India when I'd not yet unpacked and yet needed some material to read on my daily commute.

So what's dynamic logic all about? Turns out its a mathematical way of proving programs do what they're supposed to. The initial bit of the book is a refresher on the set and logic theory required to digest the rest of it, which is a whole lot of "here's how to prove that you can prove things about programs". I'm paraphrasing, obviously, but clearly it was a "How" book, not a "Why" book; which was fine because it was intended to be a textbook for Philosophy majors and CS PhDs apparently.

Since I was not reading it for those reasons, however, I applied Penrose's advice (cf Emperor's New Mind) of simply glossing over any math that I didn't understand and tried to glean the "Why" from the pile of "How". Here's what emerged:

• Dynamic Logic harbors the hope of describing programs in terms of pure logic so that you can make assertions about the outcome of running them. I'm not sure how you could do that to real world apps.
• However, the concept of attaching a first-order (or higher) predicate to a program so that the tuple (program, fact/predicate/rule) represents the duo of what the program is and what its execution means seems useful, especially in the kind of code analysis scenarios I'm interested in. It should be tempered with a suitable dose of allowance for leaky abstractions, however. Fuzzy logic maybe? I don't know.
• Nowhere in the book did I see any attempt at interpreting anything larger than one program. And its a book of about 600-700 pages.
• Towards the end was a section on Temporal Logic. This technique attempts to understand the dynamic nature of running processes by asserting their state at a particular point in time. This is markedly different from the Dynamic Logic method of analyzing the outcome of the finished process and is therefore suited to long (or always) running processes like Operating systems. To me this looked like an interesting way of modeling debugging.

I'm sure I'm missing a lot of the great parts in Dynamic Logic because of my engineering bias, but I'll take the program+fact tuple concept away with me.