¿Alguien ha creado realmente un sistema que escriba programas de computadora a partir de las especificaciones?

¿Alguien ha escrito alguna vez un sistema (software o explicación detallada en papel con ejemplos simples) que genere programas de computadora? Ingreso y crea un programa que enumera los números primos menores que 10. P r i m e ( x ) se define simplemente como 1 < x ∧ ∄ $Prime(x) \wedge x<10$$Prime(x)$ profesores dicen que pueden pero nadie da ejemplos completos reales.

Este es un tema de investigación muy activo, muy prometedor, aunque la automatización completa de la generación de programas probablemente tiene limitaciones intrínsecas (¿pero los seres humanos son mejores?). Pero la idea sigue siendo muy útil para ayudar considerablemente a la creación de programas mecanizando muchos pasos y comprobando automáticamente la corrección de la generación del programa.

Está fuertemente relacionado con un resultado en la lógica, llamado correspondencia de Curry-Howard (o isomorfismo), que muestra que los programas de computadora y las pruebas matemáticas son muy similares.

Entonces, la idea es que el sistema tomará la especificación de su programa como un teorema para ser probado. En el caso de su ejemplo, sería algo como (informalmente): "hay un conjunto de todos los números primos menores que 10".

Luego, intentará probar ese teorema, y ​​los sistemas existentes lo ayudarán a hacer la prueba, automatizar algunas partes, posiblemente la prueba completa, y asegurarse de que nunca cometa errores.

A partir de esa prueba, se puede extraer un programa que realmente calcula la lista deseada de números primos que se habían especificado inicialmente.

Varios sistemas se desarrollaron en el pasado para dilucidar estas ideas. Uno de los más conocidos fue LCF por Robin Milner , quien creó el lenguaje ML para ese propósito. Uno de los sistemas más avanzados actualmente es Coq .

Hay ejemplos completamente elaborados, algunos de ellos bastante complejos. Puede encontrar algunos en el siguiente artículo , aunque de ninguna manera es una lectura simple y requiere conocimientos avanzados de lógica.

La respuesta de wag: Sí, pero al momento de escribir, para la mayoría de los programas no triviales, las especificaciones parecen ser tan difíciles de escribir y depurar como lo serían los programas.

Más en serio, la respuesta de babou es buena, pero también voy a sugerir revisar el área de los tipos dependientes. Hay un libro bastante bueno que usa Coq (descargo de responsabilidad completo: escrito por un amigo mío), pero también hay Epigram, Agda e Idris. Isabelle / HOL también vale la pena echarle un vistazo.

Todos estos se basan en el cálculo de las construcciones. Si desea conocer la base teórica, busque la teoría de tipo Martin-Löf. Hay algunas excelentes presentaciones alrededor.

Aquí, en una tangente, los generadores de programas (es decir, sistemas que dan una descripción de alto nivel de algo en un lenguaje especial) han existido desde siempre. Cualquier compilador es uno de esos, al igual que cualquiera de los muchos generadores de analizadores. En el pasado, los sistemas llamados "lenguajes de tercera generación", que generaban (la mayoría del) código de una aplicación comercial típica dada una descripción de alto nivel y un catálogo de datos disponibles, eran populares.

La programación lógica y, en general, la programación declarativa toman como premisa exactamente lo que usted propone: es decir, a partir de una especificación lógica, devolver un resultado que cumpla con esa especificación.

Un área que parece abordar específicamente el ejemplo de "primos menores que 10" que da es la Programación de restricciones, que trata de encontrar soluciones a problemas que involucran ciertas restricciones, incluidas las restricciones de enteros como las que dio.

Es posible que desee probar ECLiPSe para una implementación específica (de código abierto) de dicho sistema.