Let's consider which are the hard parts of verifying that remote code is safe. Useful verifiers exist. Coq is a state-of-the-art verifier for a large class of

Let's consider which are the hard parts of verifying that remote code is safe. Useful verifiers exist. Coq is a state-of-the-art verifier for a large class of propositions. It hasn't been easy to create. Its design is not frozen. We need to create a specification for safe remote code that is trustworthy. This seems difficult when permitting all the remote code capabilities that we want. We need to demonstrate constructing specification-compliant code for a nontrivial algorithm with a proof of compliance. This seems costly but feasible.