The whys and what ifs of programming

I’m submitting this paper to PADL this coming Friday. Conveniently, the organisers extended the deadline by a week, so I have a few days to solicit some comments. It’s not as coherent as I would like, but for the first time I’ve got something approaching an end-to-end story: a problem, a motivating example, a solution (with formal spec), and an implementation. It’s still restricted to a first-order, call-by-value setting, allowing me to side-step the issue of code modification. (If values can have function type, and values can change, then there’s no side-stepping the issue. Ditto call-by-name, which allows values to have code in them.) I’m planning to tackle code modification next, and with that in place it should be easy enough to accommodate higher-order functions too.

I’ve narrowed my motivation down to focus on an “interactive” style of programming, where the programmer is engaged in an ongoing dialogue with the development environment, and all programming activities, including writing new code, are framed in terms of the programmer asking questions and the development environment responding. It took me a while to realise that having a narrow motivation is really the only sane methodology. If there are other applications or benefits (as I think there are) they’re best treated separately, else the whole thing gets too unwieldy. For now it’s nice to have a narrow problem to solve and a reasonably simple story to tell.

There’s not much yet in the way of theorems about formal properties of the system. So far, the formalism is really just serving as a dependently-typed programming language, only one I don’t happen to have a compiler for. Guess I should probably start using Agda.

There is some source code though. I was planning to host it on GitHub, but unfortunately I’m still running on Windows, and Git on Windows looks a bit sketchy. So I’m using Google Code. (Annoyingly its source browser doesn’t like the apostrophes I’ve used in my identifiers, so I may think again.) The code is now in F# instead of Haskell, which will hopefully make experimenting with UI ideas a bit easier. For now there’s no UI, though.

So: what are the biggest problems with this paper? I’m glossing lots of important issues, time and space performance being obvious ones, and how to recover something like normal effectful programming.

One comment

  1. Roly Perera says:

    The link now is to the submitted version. Thanks to the several people who helped me out with feedback. (They’re all mentioned in the paper.) It’s still a bit crappy, mainly the last 5 pages or so, so sorting that out is my next job.