Paper at Onward!

Jonathan's paper on Typestate-Oriented Programming (of which I am a co-author) was accepted at this year's Onward! conference. Onward! is a conference co-located with OOPSLA that promotes more radical and innovative ideas than traditional conferences, but is less concerned with theory and proofs.

This paper talks about a new programming paradigm that makes typestates (like states) a first class element of the language (called Plaid). The main philosophy behind typestate-oriented programming is that programmers these days rely heavily on libraries, and thus it is important that they use them correctly. In most cases, the correct usage of libraries (or APIs) can be specified in the form of a protocol state machine; of which a simple example is that a file can only be "read" if it's "open". By having typestate explicitly in the language we encourage library writers and users to think in terms of these states [Boroditsky], which should help them design, document, and reuse library components more effectively. Of course this also helps us statically check violations using the compiler, instead of having to run an external checker like Plural. For the complete list of advantages and more on the philosophy behind the language I encourage you to read the paper.

Currently, I am working on the type system of the core Plaid language and formalizing it in a proof-checker called SASyLF. Since I am new to language research, theory does not come naturally to me and so going's a little tough. However, at the same time I am learning a lot since the type theory here is quite advanced and formalizing everything in a proof checker forces you to get every little detail right. Hopefully, soon I will have something substantial to show for my efforts.