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/camljava

That 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.

(As an aside: the #ocaml channel is also populated by experts from the
OCaml community, so its advice is probably as good as the list.)



On Thu, Apr 12, 2018 at 11:40 AM, mukesh tiwari <
mukeshtiwari.iiitm@gmail.com> wrote:

> Hi Everyone,
> I am trying to call some Java functions from OCaml (Extracted from Coq if
> it matters). I am familiar with ocamljava [1], but it says that "*The
> generated code usually runs faster than OCaml bytecode but slower than
> native code. Memory consumption and startup time are also higher, but
> leveraging the multiple cores of a machine can help reaching the
> performance level of native code.*", and I don't want to leave the OCaml
> native code. One suggestion I got on #ocaml channel is using RPC and a
> quick Google search leads to ocaml-rpc [2].  I am wondering if experts from
> OCaml community could please give me some suggestions.
>
>
> Best regards,
> Mukesh Tiwari
>
>
> [1] http://www.ocamljava.org/
> [2] https://github.com/mirage/ocaml-rpc
>

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs