> each function is identified by a hash of its AST.
That encoding for mobile code only works if the expression has no free variables (i.e. is closed).
It turns out that it is surprisingly difficult to write code which you can be sure has no free variables at particular points (the "send this code to another machine for execution" points). Especially in functional languages. If you write a higher-order functional, you know nothing about the closedness of its argument. If you require that all function arguments be closed it breaks all the useful functional programming techniques. The only way to make it workable is to check closedness only on those values which need to be mobile.
If you do the closedness-check at runtime, toy examples will work fine and the technique looks quite powerful, but once your codebase gets to a meaningful level of complexity it turns into a game of whack-a-mole with closedness heisenbugs. You quickly discover that closedness is data-dependent.
In order to check closedness statically you need quite a sophisticated system of modal types. MetaOCaml was the most usable result of all this research:
https://okmij.org/ftp/ML/MetaOCaml.html
The important upshot here is that this isn't just some check you can slap onto the compiler. The programmer has to think about these types, and craft them carefully, as an integral part of the programming process. Basically you aren't just writing a program, you're writing a program plus a proof that it won't try to mobilize open code. Writing formal machine-checked proofs is not something that most programmers are good at.
