La verificación estática es un mal comienzo para esta tarea. Se basa en la suposición de que es posible verificar la corrección del programa automáticamente. No es factible en el mundo real, y esperar que el programa verifique código arbitrariamente complejo sin ningún indicio es simplemente tonto. Por lo general, el software para la verificación estática termina requiriendo sugerencias en todo el código fuente, y al final genera muchos falsos positivos y falsos negativos. Tiene algún nicho, pero eso es todo. (Véase la introducción a "Types and programming languages" de Pierce)
Si bien este tipo de herramientas fueron desarrolladas por ingenieros para sus propios propósitos simples, una verdadera solución se ha estado cocinando en una academia. Se descubrió que los tipos de lenguajes de programación tipados de forma estática son equivalentes a los enunciados lógicos dado que todo transcurre sin problemas y el lenguaje no tiene ningún tipo de mal comportamiento. Esto se llama "Curry-Howard correspondence", y la incrustación de lógica en tipos es "Brouwer-Heyting-Kolmogorov logic". Las pruebas más potentes solo son posibles en los idiomas con tipos potentes: dependent types. Si olvidamos toda esta terminología por un tiempo, esto significa que podemos escribir programs that carry proofs de su propia corrección, y estas pruebas se verifican mientras el programa se compila, sin ningún archivo ejecutable dado en caso de falla.
El lado positivo de este enfoque es que nunca obtienes ningún false negatives, es decir, se garantiza que el programa compilado funciona correctamente de acuerdo con las especificaciones. Incluso sin pruebas adicionales sobre la especificación, los programas en idiomas de tipo dependiente son menos propensos a errores, porque las divisiones por cero, las excepciones no controladas y los desbordamientos simplemente nunca terminan en un programa ejecutable.
Escribir estas pruebas a mano siempre es tedioso. Para eso hay "tactics", es decir, programas que generan pruebas de corrección. Estos son casi equivalentes a los programas de verificación estática, pero, a diferencia de ellos, son necesarios para generar pruebas formales.
Hay una variedad de lenguajes de tipo dependientemente-para diferentes propósitos: Coq, Agda, Idris, Epigram, etc. Cayenne
tácticas se implementan en Coq, y probablemente varios otros idiomas. También Coq es el más maduro de todos, con infraestructura que incluye bibliotecas como Bedrock.
En el caso de la extracción de código C a partir Coq no es suficiente para sus necesidades, puede utilizar ATS, el cual está a la par en el rendimiento con C.
Haskell emplea forma débil de Curry-Howard correspondencia: funciona bien, a menos que comiences a escribir programas fallidos o en bucle continuo. En caso de que sus requisitos no sean tan difíciles de escribir pruebas formales, considere usar Haskell.
¿Se refiere a un lenguaje diseñado para hacer análisis estático o para ser más fácil de analizar a través de una herramienta? Mi respuesta parece diferir de lo que otras personas quieren decir, quizás estoy equivocado, pero volviendo a leer la pregunta, hay lugar para esta ambigüedad. – jdehaan
@jdehaan, para hacerlo más fácil a través de una herramienta. En otras palabras, para facilitar el análisis de los programas * implementados en ese idioma *. No es "un lenguaje para implementar herramientas de verificación estáticas". –
Ok gracias por precisar, luego ignore mi respuesta, no es útil para usted, y además los idiomas que cité son altamente experimentales y no son útiles para otras cosas que no sean el trabajo teórico. Lo dejo tal vez alguien lo encuentre interesante :-) – jdehaan