Hace 80 años, el lógico Alonzo Church y Alan M. Turing introdujeron sendos modelos de cálculo simbólico automático (el denominado Cálculo Lambda y lo que hoy conocemos como Máquina de Turing) y avanzaron la tesis hoy conocida como de Church-Turing, que es la base de la informática moderna.
Salvador Lucas, catedrático de la Universidad Politécnica de Valencia en el área de Lenguajes y Sistemas Informáticos, explica en la sección Crónicas del intangible, de Elpais.es, que esta tesis demostró que el Problema de Decisión de Hilbert no tiene solución. En términos actuales significa que no existe ningún programa de ordenador que sea capaz de establecer si una propiedad expresada en el lenguaje de la lógica es cierta o falsa.
Eso implica que nuestras preguntas sobre el comportamiento del software y, en general de los sistemas informáticos que utilizamos, no siempre obtendrán respuesta. Tampoco significa que nunca obtendrán respuesta: hay espacio para el desarrollo de métodos que nos permitan estudiar ciertas propiedades, depurar errores y conseguir software más fiable.
