It appears some people haven't understood my comment so I will attempt to explain it more fully. First let me be clear that this comment only relates to the pa

It appears some people haven't understood my comment so I will attempt to explain it more fully. First let me be clear that this comment only relates to the parent's statement "A program could also be implemented in a safe language where the defined semantics rule out RCE." It is this claim I take issue with, not anything about the original post, which I haven't looked at in detail. Spark allows contracts and pre- and post- conditions to be defined on procedures which together may amount to encoding a spec for the application into the source code. It may then be possible to prove the implementation correct relative to this spec. But that's very different from saying that the defined semantics of the language alone (ie. without the spec which must be provided to the verifier one way or another) prevents RCE. Now to substantiate my claim that the semantics of a general purpose language cannot alone "rule out RCE". 1) A general purpose language may be used to implement a program which provides an RPC (remote procedure call) mechanism, whether open to all or restricted to a set of authorized users. 2) A program written in a general purpose language may implement an interpreter for its own, or some other language, such as Scheme. 3) In the absence of a formal spec nothing prevents the programmer from implementing an RPC call which takes a string received from the network, with no authorization/authentication checks, and runs that string through the program's scheme interpreter. This constitutes RCE by any definition I'm aware of.