Se ha demostrado que una máquina de Turing con solo 1,919 estados de control —aproximadamente equivalente a un programa en Python de 100 a 200 líneas— posee un comportamiento que es matemáticamente independiente del sistema de la teoría de conjuntos de Zermelo-Fraenkel (ZFC). Esto demuestra que incluso piezas de software relativamente pequeñas pueden alcanzar un nivel de complejidad donde su corrección no puede ser probada por los marcos matemáticos actuales, independientemente de las herramientas utilizadas.
El colapso del programa de Hilbert
A principios del siglo XX, el matemático David Hilbert buscó formalizar todas las matemáticas en un sistema consistente y completo. Creía que cualquier propiedad de un sistema formal podría ser totalmente comprendida y decidida por un algoritmo. Este optimismo fue desmantelado por los teoremas de incompletitud de Kurt Gödel y el trabajo posterior de Alonzo Church y Alan Turing.
El Teorema de Parada resultante —el primer gran teorema de la informática— demostró que no existe ningún algoritmo capaz de decidir si cualquier programa dado se detendrá alguna vez. Esto estableció un límite fundamental: algunos comportamientos computacionales son inherentemente indecidibles.
“El costo de la corrección —al igual que el costo energético de reducir la entropía— es un resultado de las “leyes naturales” de la computación, que no pueden ser evitadas de ninguna manera.”
— Why Writing Correct Software Is Hard
Cuantificando la dificultad de la verificación
La dificultad de verificar el software puede medirse a través del teorema del 'Abejorro Ocupado'. Este teorema define una función no computable que representa el número máximo de pasos que una máquina de Turing que se detiene con un número específico de estados puede realizar. Debido a que esta función es no computable, no existe un 'atajo' general o algoritmo que pueda predecir el comportamiento de todos los programas de un tamaño determinado.
Del mismo modo, el tamaño máximo de una prueba mínima de terminación para un programa de tamaño n también es no computable. Esto significa que el esfuerzo requerido para probar la corrección de un programa crece más rápido que cualquier función computable, creando un 'costo de corrección' que no puede ser evitado únicamente mediante una mejor ingeniería.
Programas pequeños e independencia matemática
Las limitaciones de la verificación de software no son solo una cuestión de escala; existen incluso en programas pequeños. Utilizando el segundo teorema de incompletitud de Gödel, los investigadores han construido programas que son 'independientes' de ZFC. Estos programas están diseñados para buscar una contradicción en los axiomas de las matemáticas; si el sistema es consistente, el programa nunca se detiene, pero este hecho no puede ser probado dentro del propio sistema.
Debido a que estos programas son pequeños —a menudo con menos de 200 líneas de código— sirven como un ejemplo concreto de cómo el software puede alcanzar un punto donde su comportamiento es matemáticamente indeterminado. Esto sugiere que, para cierta lógica compleja, la limitación no es la falta de potencia de cómputo, sino la falta de demostrabilidad matemática.
Esta imagen ilustra la frontera conceptual entre la informática y las matemáticas discutida en el artículo.
La computación como un proceso físico
Si bien estos resultados están arraigados en la lógica abstracta, están ligados al mundo físico a través de la tesis de Church-Turing. Esta tesis sugiere que cualquier computación realizada por un proceso físico puede ser simulada por un modelo computacional universal. Por lo tanto, los límites teóricos de las máquinas de Turing se traducen directamente en los límites prácticos de cualquier computadora física.
Este diagrama apoya la discusión sobre cómo la lógica abstracta se traduce en computación física.
La distinción entre las matemáticas como herramienta y la computación como un proceso físico es vital. Debido a que un algoritmo es algo que se lleva a cabo en el mundo físico, las 'leyes naturales' de la computación dictan que los programas están fundamentalmente en conflicto con la comprensión total, automatizada y la corrección absoluta.