Compilador verificante
# Compilador verificante

Compilador verificante es un gran reto propuesto por C. A. R. Hoare. En la actualidad es un reto realizar una correspondencia entre la teoría de la computación y las aplicaciones de software. El desarrollo de un compilador verificante es una herramienta esencial para reunir ambas áreas dado que pondría a disposición de los ingenieros de software los resultados teóricos alcanzados.

## Grandes retos

Un gran reto es un esfuerzo coordinado o en competencia que puede implicar logros científicos de gran envergadura y que no hubieran podido lograrse de otra forma.

* 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 (completado en 2016)
* Traducción automatizada entre dos idiomas (falló en los años 60, bastante avanzada en la actualidad)

## 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.

