Honestly, I'm a little bit surprised that this has been requested. But who am I to deny my colleagues the pleasure of what is, perhaps, the mathematically densest paper that I have ever written? For those who may not be aware, the formal semantics of a programming language is the mathematical statements about what exactly all of those pieces of code mean. And since programming languages are generally awfully complex, the formal statements of their nature are often even more so.
Except... if you do it really well and elegantly, like this Featherweight Java paper, or the R5RS manual for Scheme, then you can seize the vital core of the language in only a few operations and end up with only a page or two of dense mathematics.
This paper, though, we wanted to ensure we covered everything in the set of unusual operations that are made available and used by Proto, in its discrete approximation. This is part of a general project on formalization of concepts in space-time computing that we've been conducting over the past couple of years. We've produced formal continuous models, a prior key-operators-only discrete model, and now this full model of the discrete behavior of Proto.
It must be admitted, though, that the process of getting there has led to a paper that is sometimes colloquially referred to within my office as "the paper with the four different types of arrow."
I'm very happy with this paper, for all that I find our own work challenging to read without at least an hour to retrain the symbology into my brain. I'm also quite grateful to my coauthor Mirko Viroli, for helping instigate this and leading on the semantics development. We've ended up getting a much clearer focus on what's important and different about computations distributed over space-time: in particular, it turns out to be incredibly powerful to be able to constrain which regions of space a program runs in---and to implicitly pass that constraint down to all sub-programs within it. We've also found a number of bugs and subtleties in our prior thinking, especially to do with boundaries in space and time. And already, we are moving on, reducing these semantics to a simpler and more elegant form, that is not tied to Proto and where perhaps we can formally unify the continuous and discrete worlds... it is a hard project, but, I believe, an important one.
For those who swim well in these challenging seas... your thoughts are eagerly anticipated.
No comments:
Post a Comment