I remember as a student that I was comfortable just looking at notation and reasoning about things. CSP has a very simple notation. But after a decade as a pr

I remember as a student that I was comfortable just looking at notation and reasoning about things. CSP has a very simple notation. But after a decade as a professional programmer, I somehow lost patience for things that can't be run. Either experience taught me not to trust things that don't run, or ideas are not fun unless you can poke at them, or my mind got lazy. I just want to run things and see what happens. I like the CSP model, but since nothing can be run in this book, unfortunately I would look elsewhere to study it. I've been playing with Standard ML and it seems like a nice way to mathematically specify algorithms, but which can still also be run. Also, Leslie Lamport's style of doing mathematics with runnable proofs seems very interesting: http://scholar.google.com/scholar?cluster=14553320809011812377&hl=en&as_sdt=0,5&sciodt=0,5 http://scholar.google.com/scholar?cluster=145533208090118123...