Interview with Robin Milner

Slashdot linked to a long interview with Robin Milner, creator of ML, and known for hindley-milner type inference.

I found it interesting to read about how he moved from one area of subfield of CS to another during the 50's and 60's. I feel I'm doing the same kind of thing right now; trying to find something to concentrate on.

I never knew that ML was originally designed as a way of encoding proof strategies for a theorem prover. It makes me want to learn more about the equivalence between logic and computation. I've heard it mentioned in passing but never really studied it.

He off-handedly mentions petri nets, which I came across once a few years ago when looking for new programming paradigms (other than imperative, functional, logic, and constraint), but never really looked into.

With respect to petri nets, I was pleased to hear him point out that compositionality is important -- the lack of compositionality is my main problem with aspect oriented programming. Compositionality is basically the mathematical equivalent of divide and conquer, except that it requires proving that your division is complete, and that there are no niggling connections between the pieces you created.

Petri nets themselves seem to be mainly concerned with concurrent programming, which is not something I'm interested in, so I don't think I'll pursue that connection very far. The hope, I suppose, is that by researching concurrency, people will come up with techniques and insights that are useful for non-concurrent programming.

He then goes on to talk about things I've never heard of: CCS, Hennessey-Milner logic, bisimilarity, etc. For example, I have no idea what this sentence means: "Strong equivalence, although it was not defined in terms of maximal fixpoints, coinductively, turns out to coincide with bisimilarity. That's because of the fact of image-finite transitions."

Somehow, discussion of these Things I Don't Understand leads to discussion of how to refine a specification into an executable program, which is something I'm very interested in. So I suppose I should try to learn about the pi-calculus, so that I can follow that thread through to the punchline, which is automatic programming.

One interesting comment made in the interview is that complexity and semantics may not be "mutually explicable". That is, they're orthogonal; the semantics of some code and the runtime complexity of the same code use completely unrelated theories, and it's not clear how those theories influence each other. I don't know what to make of that, but it's very interesting. Kind of like the distinction between time and distance in physics, which weren't really unified until relativity.

My takeaway from the interview is that I should probably start by studying CCS. Apparently he's somewhat well-known for it (within the right circles), and if it's as useful as HM type inference, I should probably know what it's about.