Unknown knowns

Last night I went to see my friend Peter Alvaro give a talk based on Joseph Halpern's paper "Using Reasoning about Knowledge to Analyze Distributed Systems". There were various interesting aspects of Peter's talk, but I keep coming back to one of his closing points, "There are deep connections between semantic structures and system behavior." He followed this up with a comment which I paraphrased in my notes as "Pick a logic and find a rich correspondence between it and something in the real world, and...'profit'."

As some of you reading this well know, PL researchers like, say, Frank Pfenning have made a tremendously fruitful career out of doing exactly that. It's not a new idea. The part that is interesting and novel to me is that, this time, the person suggesting it is not someone I would pigeonhole as a PL researcher. That's important, because I think it's easy for beginning PL researchers like me to walk around self-importantly thinking that we are the only ones who think this way. But we're just not. Like petulant teenagers, we like to insist that nobody understands us, and certainly nobody at Berkeley understands us, but it's not true and we should knock that shit off.