Comcert is verified functional code in coq that is translated to ocaml for execution, the compiler for which isn't verified. It doesn't solve the problem of ver

Comcert is verified functional code in coq that is translated to ocaml for execution, the compiler for which isn't verified. It doesn't solve the problem of verification of imperative code. The state of the art approaches to imperative code verification using coq ( such as https://gitlab.mpi-sws.org/iris/refinedc https://gitlab.mpi-sws.org/iris/refinedc ) struggle to verify the basic college textbook algorithms and are extremely clunky in practice.