En un artículo técnico extenso, un investigador especializado en verificación formal argumenta por qué Rocq sigue siendo, en su práctica diaria, una herramienta más adecuada que Lean para la verificación de programas, aunque concede que Lean ha ganado tracción en la formalización de matemáticas, sobre todo tras los recientes avances de la IA en este campo. El texto compara ambos asistentes de pruebas a partir de varios ejes.
El primero es el tratamiento de tipos codata y cofixpoints. Rocq ofrece CoInductive y CoFixpoint como declaraciones de pleno derecho, con extracción a OCaml y soporte para declaraciones mutuas, indexadas y sin parámetros. Lean incorporó en la versión 4.25 la palabra clave coinductive para predicados coinductivos, útil en bisimulaciones, pero no genera cofixpoints ejecutables. El experimento más cercano a Rocq, QPFTypes de Alex Keizer, es explícitamente un prototipo y presenta fricciones al abandonar casos simples: no acepta declaraciones sin parámetros, ni coinductivas mutuas, ni familias indexadas, obligando a recurrir a la API de bajo nivel MvQPF.Cofix.
El artículo examina además las alternativas que usan a diario los programadores de Lean para reproducir este comportamiento: Stream' de mathlib (resuelve solo streams, no codata arbitraria), Iter (interfaz de iteradores con pruebas de productividad), Thunk (aporta pereza pero no coinducción) y partial def, que oculta el cuerpo recursivo tras un opaco y limita el razonamiento sobre él. En cambio, un cofixpoint de Rocq, tras superar el comprobador de guarda, extrae directamente a un valor perezoso observable.
El autor ilustra la relevancia del asunto con bibliotecas como Interaction Trees, que en Rocq representan programas con efectos como árboles coinductivos sobre los que se puede programar, interpretar y extraer código. Por contraste, el panorama en Lean exige combinar codificaciones genéricas, iteradores explícitos o funciones parciales opacas para acercarse al mismo resultado.