Announcing the 2015 edition of the OBT workshop, to be co-located with POPL 2015, in Mumbai, India. Two-page paper submissions are due November 7, 2014.
From the web page (http://www.cs.rice.edu/~sc40/obt15/):
I am slowly working my way up to an understanding of separation logic and one thing I have not seen with separation logic is a transformation into functional code with immutable data structures.
With normal imperative code you just wrap a big fat monad around everything and there is a straightforward transformation into functional code with immutable data structures.
The disadvantage of a big fat monad is that you loose the ability to reason about parts of the program that have side effects but are independent of each other. I would expect therefore that smaller monads that could be split and combined by the rules developed for separating logic and the separating conjunction would exist.
Does anyone know if anyone has already research that? Or perhaps I am making an elementary error in my reasoning?
I'm trying to decide how I want to approach the issue of immutability in my language. So far, I've identified three general approaches.
Obviously, there are the purely functional languages, in which there is no mutability at all. I'm not interested in that approach, mainly because my focus is on multi-paradigm programming and that approach is too narrow for me.
The second approach is that used by C++, where 'const' is a type modifier - that is, a mutable type can be declared read-only after the fact.
The third approach is that taken by Java and many other languages where there are separate mutable and immutable types, which may conform to a common interface but which have separate implementations. For example, you have ArrayList and ImmutableList, both of which implement the List interface.
An advantage of the Java approach is that the immutable implementations can in many cases be simpler and more efficient than their mutable counterparts. A case in point is ImmutableList, which has an optimization whereby empty lists are represented by a reference to a static singleton instance.
On the other hand, it's extra work to have to implement two versions of every collection. That extra work isn't a problem for the most commonly-used containers, but for the long tail of specialized and possibly application-specific types it can be a significant burden.
C++ on the other hand has it's own version of the 'double work' problem, whereby a lot of classes end up having to implement two versions of many methods, a 'const' and 'non-const' version. However, this can be solved by language design - a 'conditional const' type modifier which is const only if the enclosing type is also const. This allows many of these double-definitions to be collapsed.
However, you still have the problem of maximizing efficiency of container implementations. Suppose I have a C++ class X that internally contains a vector. Adding the const modifier to X doesn't switch the implementation of the vector over to a more efficient, immutable version; And even if the language supported it, it wouldn't be very efficient because now you have to add a level of indirection between X and the vector (using virtual methods or some other technique) so that X's implementation can switch between the mutable and immutable implementation of vector based on whether X is mutable.
So I'm wondering if there are any other interesting approaches out there, or if there's a sweet spot that I'm missing.
As of about a week ago, Jonathan Blow (creator of various well received games such as Braid as well as various PL efforts) has pair of talks on twitch.tv (later both put on youtube) where he issues a call to arms for game developers to design a new programming language around their concerns. He discusses what he sees as some of the shortcomings of existing languages that are supposed to be C++ replacements, and some of the requirements he feels game devs have. There was a Q&A session as well.
Meredith tweets under the handle @maradydd and contributes much to the tiny niche comprising the intersection of type theory and security. For example:
The presentation of Kaya at the Future of Programming Workshop at the Strange Loop conference.
Kaya is declarative like SQL, reactive like a spreadsheet, and a spreadsheet metaphor is used to render powerful, expressive data structures. Code is not written in a text editor, but instead you compose applications in a spreadsheet-like editor. The resulting contextual nature ameliorates some of the typical need for control structures, and leads to a more natural way to compose applications.
Evan's (the Elm guy) strangeloop talk, it is actually quite good (and not bad for Prezi); slides:
Video of talk:
A very nice (and useful) overview about the different flavors of FRP.
Axiomatic language is a formal system for specifying recursively enumerable sets of hierarchical symbolic expressions. But axiomatic language does not have negation. Extended axiomatic language is based on the idea that when one specifies a recursively enumerable set, one is simultaneously specifying the complement of that set (which may not be recursively enumerable). This complement set can be useful for specification. Extended axiomatic language makes use of this complement set and can be considered a form of logic programming negation. The web page defines the language and gives examples.
I recall there was an article on LtU that defined term syntax sugar. IIRC the generic idea was that syntax sugar requires only the local transformation. And language features that require non-local program rewrites cannot be called syntax sugar and it can be core of argument that one language is higher-level then another.
Active forum topics
New forum topics