Los verificadores de tipos no solo evitan errores de programación como sumar cadenas y enteros, sino que además sustentan los asistentes de demostración, lenguajes como Lean y Rocq que validan matemáticamente teoremas. La base de esa capacidad es la correspondencia de Curry-Howard, que establece una equivalencia entre pruebas y programas: demostrar una proposición equivale a construir un valor del tipo correspondiente, la conjunción lógica se traduce al producto de tipos, y la implicación a funciones entre tipos.
El artículo ilustra ese mecanismo con un teorema elemental en Lean: la hipótesis fija dos números naturales y el objetivo es demostrar que la suma es conmutativa. La prueba se reduce a deconstruir el objetivo, instanciar la hipótesis adecuada y aplicar los constructores sucesivamente, momento en el que Lean muestra un mensaje de éxito.
La limitación aparece cuando el verificador de tipos evalúa las expresiones para garantizar la corrección de la prueba. Si una expresión no termina, el verificador no puede decidir. Turing demostró en 1936 que el problema de la parada es indecidible, así que los lenguajes formales restringen sus construcciones, por ejemplo exigiendo recursión acotada, para asegurar la terminación. Esa restricción tiene un precio: la incompletitud, descrita por Gödel, implica que todo sistema formal consistente capaz de aritmética básica deja enunciados que no puede demostrar ni refutar. En consecuencia, siempre habrá teoremas que escapen a la verificación automática.