Un quine construido desde el segundo teorema de recursión de Kleene
Constructing a Quine from Kleene's Second Recursion Theorem
Los quines existen como corolario del segundo teorema de recursión de Kleene, pero llevarlo a la práctica no es trivial. El autor formaliza la construcción en Rocq siguiendo un preprint que la desarrolla en el cálculo lambda sin tipos, usando codificaciones de Church para representar el AST del propio lenguaje y un quasi-quoter que convierte citas simples en citas dobles. El resultado es un quine explícito en notación de de Bruijn, y de paso una conexión con el lema diagonal de Gödel y Tarski.
Lejos de ser una tarea mecánica, el acto de formalizar puede ser en sí mismo una fuente de intuición y creatividad; por eso creo que la visión popular de la verificación formal como un mero ejercicio de transcripción yerra el blanco.