Rocq Prover: 40 años de verificación formal, un nuevo nombre

Después de más de 40 años de investigación, el sistema de verificación formal conocido anteriormente como Coq Proof Assistant ha sido renombrado como Rocq Prover. Desarrollado inicialmente en 1984 por Thierry Coquand y Gérard Huet en INRIA-Rocquencourt, y posteriormente ampliado por Christine Paulin, Rocq permite la definición de estructuras de datos, funciones, predicados, la formulación de teoremas y la verificación formal de programas. El sistema, escrito en OCaml y distribuido bajo la licencia LGPL, facilita la extracción de programas certificados a lenguajes como OCaml, Haskell o Scheme, y cuenta con una amplia comunidad de más de 200 colaboradores. El cambio de nombre busca honrar el lugar de origen del proyecto y evoca conceptos de fuerza y solidez. El sistema, en su iteración anterior como Coq, recibió prestigiosos premios como el ACM Software System Award en 2013 y el Open Science Free Software Award en 2022, reconociendo su importancia en el campo del software de investigación y la formalización matemática.