Compilador verificante

Compilador verificante es un gran reto propuesto por C. A. R. Hoare.

(Extracto de su presentación pública en Leiden, en 2003.)

Grandes retos

• Demostrar el último teorema de Fermat (cumplido)
• Llegar a la luna en 10 años (cumplido)
• Curar el cáncer en 10 años (fallido en los años 70)
• Crear el mapa del Genoma Humano (cumplido)
• Crear el mapa de Proteoma humano (demasiado difícil por el momento)
• Encontrar el "Bosón de Higgs" (en progreso)
• Encontrar las ondas gravitacionales (en progreso)
• Unificar las cuatro fuerzas de la física (en progreso)
• El Programa de Hilbert para los fundamentos de la matemática (abandonado en los años 30)

Grandes retos en computación

• Probar que P es diferente de NP (abierto)
• La prueba de Turing (no alcanzado)
• El compilador verificante (abandonado en los años 70)
• Programa campeón en Ajedrez (completado en 1997)
• Programa para jugar al Go a nivel profesional (demasiado difícil)
• Traducción automatizada entre dos idiomas (falló en los años 60)

Características de un gran reto

• Proyecto para al menos quince años
• Participación mundial
• Criterios claros de éxito o fallo
• Avances fundamentales en ciencia o ingeniería

Condiciones necesarias

• Suficiente madurez en el área
• Apoyo general de la comunidad científica
• Compromiso sostenido de los entes participantes
• Conciencia de la importancia de parte de los organismos de financiación

El compilador verificante

• El compilador verifica la corrección de los programas con respecto a su especificación.
• La especificación viene dada como aserciones en el programa, información de tipos, etc.
• Las herramientas utilizadas para la verificación son herramientas de soporte al razonamiento matemático y lógico.

Este es un reto que fue formulado ya por Turing (1948), McCarthy (1962), Floyd (1967), etc.

Representa un logro ingenieril de algo que en algún momento se consideró inalcanzable o impráctico.

Medida de éxito

• Verificación mecánica de un conjunto de ejemplos representativos de herramientas de software mecánicamente verificadas.
• Cada ejemplo producido debe ser capaz de reemplazar un software existente en su uso rutinario, de manera de servir de base para futuros desarrollos.
• Un verificador prototipo debe estar disponible para la comunidad.

Hoare propone como mínimo la verificación de corrección y terminación de aplicaciones de al menos diez mil líneas, y con un nivel menor de seguridad hasta el tratamiento de aplicaciones de al menos un millón de líneas.