NEPLS submission

I submitted the following to NEPLS:

Co-action

Co-action is a new form of synchronous reactive programming. From the programmer’s point of view, all actions take place simultaneously, and all interdependencies between actions are resolved instantaneously. Eliminating execution order avoids many of the complexities and pitfalls of imperative programming. What is novel is that co-action also supports an imperative model of state, with a heap of dynamically allocated objects pointing to one another, and assignment through pointer variables. Other forms of declarative programming either eliminate pointers or fall back to explicitly ordering execution. Co-action attempts to combine the best of both declarative and imperative programming.

Declarative languages avoid pointers for good reason: to determine a correct execution order, data flow dependencies must be known, but pointer aliasing makes that undecidable at compile time. Co-action instead finds a correct execution order at run time by monitoring program execution and doing rollbacks to backtrack. The undecidable problem at compile time is converted into a search problem at run time. Co-actions are in a sense the dual of transactions, combining synchronous actions instead of isolating asynchronous actions, and parallelizing instead of serializing.

To better study and communicate these ideas, I have defined a small formal calculus. The correctness criterion of an execution order is coherence: every field is written at most once, and prior to any reads. The completeness theorem states that if a coherent execution order exists, then the co-action execution algorithm will find it. As of this writing I have been unable to prove completeness, and am seeking advice.

6 Replies to “NEPLS submission”

  1. The abstract reads very well, although unfortunately I don’t know enough about the topic to evaluate the idea itself. The point about pointers is interesting and well-made. You’ll be in good FRP company with Shriram Krishnamurthi and Paul Hudak, so good luck!

    Overall I prefer the tone and style of this to what I read in the earlier Coherence paper. It’s more coherent :->

  2. I have to agree with Roly – this abstract makes the concept very clear. I hope to see your calculus some day.

    Not sure how difficult the proof will be, but have you tried showing it is undecidable? That might be simpler and then you know you don’t need to search for a proof.

    1. Undecidability has to due with pointer aliasing. Finding a program sequence that is the same ‘as if’ its source text was directly executed, is a different challenge. Completeness refers to the idea that the programming language should always be able to find a correct program ordering at run-time, if one exists, given an infinite amount of time. Once you have that, then you can start annotating the program (and the VM it gets loaded into) with hints for optimization that reduce the search space for a valid program and turns the JIT compiler into a correctness verifier rather than a solver; the difference between verification and solving will be fluid.

  3. Your ideas are interesting. I think that there are two reasons why they aren’t the success you’d like them to be:

    1) you don’t provide enough use cases
    2) you don’t have a working demonstration

    For example, for coherence you pretty much only have the “tasks” example. While this example works, it isn’t convincing. You could solve it by just removing the length setter. Yes, this is not as nice as your solution, but nobody is going to use a new language to get a little bit nicer answer to this problem. You need bigger and more general (argue why coherence is applicable to a class of programs) examples to warrant a new language.

    Another way to lower the barrier of acceptance is to integrate your ideas into an existing language (if possible), like the Flapjax guys are doing to FRP.

    A prototype that demonstrates your ideas in practice would help a lot too. If you have more convincing examples there might be other people who’d be interested in implementing one.

Comments are closed.