Remote procedure calls are a generic solution to cross-language computations that works in many settings. It is a perfectly reasonable thing to do.
Another option is to use Foreign Function Interfaces on both sides to do cross-language computation in a single system process (instead of RPCs and communicating processes). For Java, the FFI layer in the JNI (Java Native Interface), and there exists a library to make OCaml and Java functions communicate through the JNI (without changing the OCaml compilation backend):
https://github.com/xavierleroy/camljavaThat said, this library seems to currently lack active users, and in particular nobody did the work of packaging it on opam (
https://github.com/ocaml/opam-repository/issues/7519 ). If you are willing to give this library a try, it could be a useful thing to contribute.
In either cases, I would recommend being very careful in designing the interface between Coq code and untrusted code (pure OCaml, or OCaml+Java code using whichever coordination system). It is easy to shoot yourself in the foot by exporting untrusted functions with an optimistic type (eg. using the Coq function type for the untrusted functions that may not be total / strongly terminating). If you can design the interface between Coq and untrusted code as primarily based on exchanging ground *data* (events, queries reified as algebraic datatypes...), with an explicit loop orchestrating the coordination between both, you can get a system where the correctness guarantees (or lack thereof) are much easier to reason about. Incidentally, this design also makes the in-process data exchange more similar to what an inter-process communication system would look like, so it allows implement both solutions (in-process or remote communication) against a single Coq codebase, with minimal changes.