Los lenguajes de programación vienen en «dos sabores», intérpretes y compiladores. Los primeros, los intérpretes, obligan al sistema a analizar cada línea de código a ver si está correctamente escrita y si es así, ejecutar lo que el programador quiere. Si por alguna razón el sistema regresa a esa línea, tiene que volver a verificar que está bien escrita, aunque ya lo haya hecho antes. Por otra parte, los compiladores, traducen a código de máquina las instrucciones del programador. Así, el compilador genera un código que, en principio, corre unas 10 a 100 veces más rápido que la versión interpretada.
Pero claramente, los programas que en general se escriben, resuelven problemas administrativos, financieros, o bien se usan para jugar, etcétera. Sin embargo, hay aplicaciones que concretamente tienen que correr correctamente porque pudiese estar la vida de alguien en juego. Pensemos por ejemplo en programas que llevan el control de un marcapasos, el cual no pude funcionar mal, no puede tener «bugs» que pongan en peligro la vida del paciente. O pensemos en un programa que corre en un dispositivo como una consola electrónica que usan los buzos y que da los parámetros para saber qué tan rápido debe subir a la superficie para no sufrir problemas por una mala descompresión.
Y esto hace pensar que una cosa es hacer un programa que haga cálculos para -digamos- controlar la contabilidad y otra cuando se pone en juego la vida de alguien. ¿Podríamos confiar entonces en que el compilador va a traducir correctamente el código? La pregunta puede ser muy sensible en algunos aspectos y hay quien trabaja ya en este tema.
Así, se ha desarrollado el compilador COMPCERT, el cual es un compilador formalmente verificado, lo que significa es que hay una prueba matemática que indica que al escribir código en C, se traduce correctamente a lenguaje de máquina. El compilador puede generar código para PowerPC, ARM, RISC-V y x86, el cual acepta un subconjunto del ISO C 99 con un par de extensiones. Es claro que este compilador probablemente no pueda generar código tan rápido como el gcc, pero lo que sí vale la pena destacar es que el código creado cumple con las especificaciones dadas.
Hay que reconocer que la idea de COMPCERT es buena, pero no hay garantía que un programa escrito con este compilador va a correr correctamente. Por ejemplo, si ponemos «x=1/A», donde A es una variable entera y en algún caso, dicha variable se vuelve cero, tendremos un error y un problema con nuestra lógica en el software. Esto no es atribuible directamente al compilador. Vamos, es un error del usuario.
Para que un compilador de estas características pueda funcionar, se tienen que poner algunas restricciones, que en algunos compiladores se llaman «directivas», pero que aquí no son opcionales. Por ejemplo, arreglos de longitud variable no están permitidos y no se puede usar longjmp ni setjmp. Hay restricciones en el caso de la instrucción «switch» también. Sin embargo, hay una variedad de opciones que permiten examinar el código corriendo a través de un intérprete.
Y más de uno podrá pensar que los compiladores normalmente traducen correctamente, pero la realidad es que en la documentación de los compiladores, se han hallado artículos (de 1995 al 2011), en donde se ha hallado errores en la forma de compilar, incluso en los compiladores más populares.
Para que el COMPCERT funcione correctamente, un asistente de la prueba matemática del código compilador checa el código pasando por el mismo en 15 ocasiones, y todas deben probarse como correctas. Incluso así, hay un 10% de código que se ha demostrado que no es correcto. Los desarrolladores de COMPCERT dedicaron 6 años de procesamiento de máquina paras hallar errores de compilación usando Csmith y no pudieron hallar ningún error, cosa que no fue así considerando otros compiladores.
Esta idea de los compiladores verificados es interesante aunque quizás no es necesaria en la mayoría de las aplicaciones. Sin embargo, es un paso para hacer que formalmente los compiladores sean herramientas más sólidas.
