Grail: a functional form for imperative mobile code. In the novel by {it R. L. Stevenson} [The strange case of Dr. Jekyll and Mr. Hyde. London: Longmans, Green (1886)], Dr. Jekyll is a well-regarded member of polite society, while his alter ego Mr. Hyde shares the same physical form but roams abroad communing with the lowest elements. In this paper we present Grail, a well-behaved first-order functional language that is the target for an ML-like compiler; while also being a wholly imperative language of assignments that travels and executes as Java classfiles. We use this dual identity in the Mobile Resource Guarantees project, where Grail serves as proof-carrying code to provide assurances of time and space performance, thereby supporting secure and reliable global computing.