If one were to examine computation in X, what properties hold?

If we ignore objects in the language, computations are deterministic. This will be demonstrated by breaking computations down into a series of steps and examining the results of each step. If each step is deterministic then the whole computation is deterministic. But what about steps being executed in parallel by an adversary scheduler? I'll show that even if you don't know the whole state of the machine at once, you can always predict the pieces of state that could possibly be needed by the current step.

The absence of "mutable shared state" will be key to the proof. In X, we promise to the user that there is no such thing as shared state between concurrently executing threads, except in the context of objects and their member variables. We will prove this by examining each syntactic form in the language and showing that it cannot create a reference shared with any component that could execute at an unknown time (again, in the absence of objects). If this property holds, then we guarantee that at each step, all references available to the step are either to immutable objects or to mutable unshared objects.

Now, if the reference is to an immutable object, then it must be in a known state: the state it was created in. If the reference is to a mutable unshared object, then it must also be in a known state: the state obtained by starting with the state it was created in, then applying all operations to it in order up to the current step. Since the object is unshared, there is no point where the order of operations is ambiguous. Thus all references are in a known state at each point and thus the computation is deterministic.

We would also like to show that each task, once started, is wait-free: it completes in a finite number of steps (it never has to wait for another task). Tasks may be spawned by other tasks (via send), optionally passing futures. The task is never started until all the futures in its arguments are filled.

This proof is simple, as there are no waiting constructs in our language. In order to "wait" for the value of a future, you have to make a new task which receives the value.