# Coq/Ocaml project using heuristic function written in C?
**URL:** https://discourse.rocq-prover.org/t/coq-ocaml-project-using-heuristic-function-written-in-c/2185
**Category:** Using Rocq
**Created:** [January 22, 2024, 10:35am UTC](https://discourse.rocq-prover.org/t/coq-ocaml-project-using-heuristic-function-written-in-c/2185 "2024-01-22T10:35:30Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@zyang](https://discourse.rocq-prover.org/u/zyang)
#### Post date: [January 22, 2024, 10:35am UTC](https://discourse.rocq-prover.org/t/coq-ocaml-project-using-heuristic-function-written-in-c/2185/1 "2024-01-22T10:35:30Z")
Hi,
I’m writing to seek some knowledge/suggestions about the building system of Coq/OCaml:
I’m implementing a compiler pass for CompCert. This pass uses a heuristic to optimize a program (which does not influence the correctness proof).
We have an existing implementation of this heuristic in C, but not in Coq. The specification of this heuristic is as simple a function from a list of numbers (_positive_ type) (or pairs of numbers) to another number
One thing I learned is that there exists support to use a C function in an OCaml program. Since the CompCert project written in Coq will eventually be converted to an OCaml program, I believe this could be a way we can directly use that heuristic in the C version, instead of re-implementing it in Coq.
However, I barely have developing experience in OCaml projects and I’m not very familiar with its building system, and no idea how to actually implement an OCaml program that uses C function. (And I’m even doing this in a Coq project)
So I’m posting this to seek help and suggestions on where should I get started to learn so I can eventually connect my implementations and make them a compilable/executable project.
Thank you!
---
### Author:  [@ybertot](https://discourse.rocq-prover.org/u/ybertot)
#### Post date: [January 23, 2024, 7:17am UTC](https://discourse.rocq-prover.org/t/coq-ocaml-project-using-heuristic-function-written-in-c/2185/2 "2024-01-23T07:17:16Z")
First thing, I would look at the following documentation: [OCaml - Interfacing C with OCaml](https://v2.ocaml.org/manual/intfc.html)
Second thing, I would be careful that Coq-extracted programs may use they own notion of integers (Ocaml integers are 31-bit or 63-bit, bounded integers, while Coq sometimes unbounded integers, which would be extracted to Coq as a different datatype), you will need to pay attention to this when converting the integers from C to data that your version of CompCert can use.