Lambda the Ultimate

Consider looking into the motivations around E language. Browse www.erights.org. Object capability model achieves security without a 'sandbox', and is suitable for general purpose use.

The work on the Object Capability Model is sufficient for many purposes, minus confinement (for purchased scripts, to keep them from phoning home, leaking your strategies and other secrets). Confinement is achieved by construction (as per the KeyKOS factory) or by analysis (check to see if any objects are named within the script).

A complete security solution also needs rights amplification mechanisms such as sealers/unsealers, along with blinding, and certificates for offline and transferable rights.

Resource management and process accounting is a problem that is more difficult to deal with. Even a total function (guaranteed termination) can be told to number-crunch the Ackermann functions, so you can't simply depend on such termination. It would be wise to design the language such that partial failures are part of the language model, which would allow you to kill processes and already have well-defined behaviors for the other processes that were interacting with them. Adding resource management features to the language is also possible, though I've not yet found a satisfactory approach in my own work.

I'm working on a language intended for distributed data fusion, command and control, and creating large persistent peer-to-peer virtual worlds with the same level of interconnectedness as the Internet. Its design is already sufficient to meet the various goals you've described, minus full control over resources, and plus a few design criterion for distributed development and operation. It's still a few years from completion, though, since I can't dedicate much time to its implementation.

it seems to me that the right language to allow such a system would have the ability to control effects, but do so at a very granular level

For the purposes you named above, controlling effects isn't all that useful. It's useful for other purposes, but I'll get to that below.

For the purposes in the OP, controlling effects was just a limited way to control capability. Languages designed to support capability models can do so far more readily, at a finer granularity, adding new capabilities on-the-fly as required.

Password capability and object capability models are the most promising for this purpose. Password capability is based on certificates (i.e. I can do X because I have this certificate signed by someone you respect that says Dave can do X and I can prove I am Dave if challenged). Object capability is based on encapsulation of unforgeable object identifiers (i.e. I've already proven I can do X because, if I couldn't, then the message telling you to do X wouldn't have reached you). These approaches can be used together effectively: these two approaches have disparate strengths and performance when it comes to offline use and exclusive or transferable rights (such as e-scrip).

Controlling effects (including IO, delay, divergence or non-termination, observable concurrency and race-conditions, deadlock, and non-atomic failure) has many advantages for language design. Code guaranteed to be without a given effect is usable in a wider variety of contexts, may be subject to certain optimizations, and so. If guaranteed by construction, the features don't require intelligent analysis. Controlling effects is worth doing to support reasoning about black-box composition. Since black-box composition is exactly what is happening when adding user-code to servers, I would recommend controlling effects even if it isn't much help for security or resistance to Denial of Service attacks.

What kind of language is this? What real-world examples are there that do this or what papers describe such systems?

I think the Google App Engine's Python support falls in the area you mention. The analog of your virtual world is the web itself. They've also recently announced a Java runtime as well. Both runtimes as sandboxed. For example, file system access routines in python don't work, but they provide a "data store" that scales on google's server infrastructure.

Note: I don't work for google.

The Second Life virtual environment runs user-created scripts are run on the Second Life servers. They started out with a custom-built scripting engine but they've been switching over to using Mono.

http://wiki.secondlife.com/wiki/Mono

They demoed Mono support several years ago, showing how much faster it was than their custom engine (JITed vs. interpreted). But I bet their custom engine was designed from the start to support running a massive number of scripts in isolation, whereas Mono was not. Maybe this is why Mono support is still in beta -- retrofitting lightweight isolation is not easy.

I'm not sure Tcl does all of what you want, but its sandbox is a pretty good one, and well worth checking out.

http://www.tcl.tk/man/tcl8.5/TclCmd/interp.htm

For instance, see 'resource limits'.

Furthermore, it's a mature, well-tested implementation.

I highly recommend looking at two systems/languages from the early 90s that attempted to address exactly the scenario you're talking about, though on a smaller scale.

http://en.wikipedia.org/wiki/MOO

and

http://en.wikipedia.org/wiki/ColdMUD

Both were network available user-programmable multiuser systems, meant to run MUDs, though there was really no limitation in that direction. They were both based on classless object-oriented (prototype oriented) programming languages roughly in the C & Algol syntax tradition. The initial developers of the systems were well versed in Lisp & Smalltalk, and it showed.The latter was an offshoot of the former.

To support multiuser access, there were three things at work:

* A custom language & VM, which had its own (primitive) timeslicing. All user programs were time-boxed to run a maximum amount of time, preventing them from hogging system resources.
* Prototype-inheritance object model to allow for more flexible re-use models. The "world" was full of "generics" which people could clone or inherit-from.
* Programming model which had security concepts built in. They had either Unix-style ACL security (MOO) or heavy encapsulation (law of demeter style) (ColdMUD). In fact, developers wrote capability-oriented security in the latter.

IMHO these systems were a path-not-taken; user programmable systems which mixed both synchronous ("chat) and asynchronous ("email") modalities, and encouraged users to author in the world. They were popular pre-WWW (1990-1994) and essentially lost their momentum when the web boom happened. Apart from their text only nature, they make contemporary "social computing" ala Twitter, Facebook, etc. look rather micky mouse.

Worth a look.

It might be worth asking yourself why you want a general purpose language for your users. Not all DSLs try to be complete, and there are advantages to restricting yourself to a non-complete core language. In particular termination is tricky to prove in general purpose languages (for your cpu usage guarantees). So there are two ways to attack the problem:

1. Go for a restricted DSL, one common choice is to restrict loop bounds and data sizes to constants. Each program now trivially terminates, although computing tight bounds can still be tricky (but doable).

2. Give the user a general purpose language, but use a Termination Analysis. If the analyser can prove termination then allow the program, otherwise reject it back to the user. The problem with this approach (from experience) is that you need to be an expert in writing termination analysers as well as in the domain that you are working within.

If your target audience can be satisfied by door number one, then it is a much easier way to go. Thinking through your problem domain (numerical analysis on trading patterns) I can't think of any sample program that requires arbitrary data sizes or runtime. Users will probably want to operates on fixed size widows of data, rather than on some arbitrary amount.

Door number two is more difficult but you may want to consider Proof Carrying Code as a solution. The client generates a proof that the code lies within some bounds for memory and/or runtime. The server checks the proof against the code. One system that does this for real is CaioCC, slides for a paper on the subject can be found here.

In general a lot of identical issues crop up in Mobile Programs. The problem that you've described is in fact a Mobile Program problem, but with a single fixed network topology. Issues of cpu/memory bounds on mobile code and designing DSLs to enforce them have been looked at quite extensively in that area, although the results may not show up when you search for these issues in general. Here is a good starting point that combines PCC and Mobile Code.