Gallina, the programming language underlying Rocq, has relatively efficient evaluation mechanisms. But sometimes this is not enough: we would like to write some computationally intensive part in a more suitable, off-the-shelve language. I will demo and discuss our current prototype which extends the Rocq kernel to allow declaring and calling native foreign functions. On the user-facing side, it rests on a monad similar to Haskell's IO, featuring unbounded iteration, error, imperative buffers and, well, foreign function calls. To allow reasoning on this monad we provide a weakest precondition program logic defined using Iris. This logic is already flexible enough to axiomatize the specification of most integer functions in GMP[0] and we hope to interface it with existing Rocq semantics for other languages such as C with VST[1] or Capla[2].
[0] https://gmplib.org/
[1] https://vst.cs.princeton.edu/
[2] https://fresco.gitlabpages.inria.fr/capla/language/index.html