title: Compilador verificante
text: # 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.
  
  