Calling extractable side-effect ocaml functions in Coq

Ecosystem
,
1

I’d like to reason about Coq code that will eventually be extracted to OCaml. As a result, I’d like to be able to write Coq code that can generate side-effect OCaml code that calls functions like print_endline.

Digging through these papers for CoqOfOCaml (https://inria.hal.science/tel-01890983v1/document, https://v2.ocaml.org/meetings/ocaml/2014/ocaml2014_15.pdf), it seems like there is some library called “Pervasives” that can be used like this. However, looking at the repository, it doesn’t seem like this is the case anymore.

I’m thinking that I might be able to write an axiom like:

Axiom print_endline : string -> unit.

that would get lifted automatically to OCaml’s print_endline. Am I on the right track, or is there a more elegant approach I can take?

2

You might be interested in FreeSpec, a framework that targets specifically this use case. It works well with coqffi for extracting purposes. For instance, I’ve built an overly simplified HTTP1.1 server and proved some stuff about it.

2 Likes