Este artículo examina las distinciones fundamentales entre la teoría de la prueba y la teoría de tipos dependientes (DTT) en el diseño de probadores de teoremas interactivos. Si bien varios sistemas implementados están diseñados utilizando el cálculo λ tipado dependientemente para representar pruebas, ningún asistente de prueba importante se ha diseñado utilizando la teoría de prueba estructural moderna, aunque, como argumentaré aquí, el cálculo secuencial ofrece un marco alternativo convincente. Se proponen seis temas específicos donde la perspectiva de la teoría de la prueba es argumentablemente superior a la perspectiva de la DTT. Estos temas incluyen la separación de la lógica de la estructura de prueba, el uso estratégico del no determinismo en la reconstrucción de pruebas, y la evitación de problemas complejos de disciplina de tipado como los niveles de universo y la irrelevancia de la prueba. El tema final —el tratamiento de uniones— se desarrolla más para demostrar cómo se logra un enfoque natural e intencional a través de la movilidad de los enlazadores. Esta metodología se ilustra mediante el probador de teoremas Abella, que aprovecha la sintaxis de árbol λ y el cuantificador ∇ para proporcionar un entorno elegante para razonar sobre la meta-teoría de lenguajes y lógicas que involucran uniones complejas.
Dale Miller (Sábado) estudió esta cuestión.