My goal is to be able to use CompCert, a certified compiler.
It is a compiler whose passes are formally verified to not introduce change in the semantics from the C code to its translation in asm.
Good luck to add/enable your fav compiler to Haiku!
You are probably aware but there was a port of ocaml to haiku before. It even has somewhat working haiku bindings. Perhaps it is outdated or not fully working, though.
It will be great to have compcert available. A truly impressive piece of engineering.
Had to follow the link to the blog post to see from who this was (the gtksourceview4 should have gave that away when I saw it) 
Congrats on the progress @Anarchos ! 
Long road ahead…
Yes, but the recent versions of ocaml have disabled the native compilation, which is mandatory to compile coq. So i have to rebuild myself the OCaml compiler with native compilation enabled.
Thanks Begasus, i could not have compiled gtksourceview3 without your help.