ABSTRACT. I propose a talk to open a discussion about this topic. My submission details the motivation and the context. Briefly, oracles are a key ingredient in the success of CompCert. Such an oracle is an untrusted foreign code which outputs are checked by certified code. However, in CompCert, oracles are currently invoked through an unsafe FFI. I will illustrate some pitfalls of this FFI and propose how to overcome them. Moreover, I will conjecture that by using an adequate FFI, we can derive ``theorems for free'' a la Wadler in Coq from the Ocaml type of polymorphic oracles, and thus discharge a part of the certification on the Ocaml typechecker. However, my proposal raises more issues than it solves: in other words, it opens a new topic of research.