Alguém realmente criou um sistema que grava programas de computador a partir da especificação?

Alguém já escreveu um sistema (software ou explicação detalhada no papel, com exemplos simples) que gera programas de computador? Eu introduzo e ele cria um programa que lista os números primos menores que 10. é simplesmente definido como professores dizem que podem, mas ninguém dá exemplos completos reais.$Prime(x) \wedge x<10$$Prime(x)$

Este é um tópico de pesquisa muito ativo, muito promissor, embora a automação completa da geração de programas provavelmente tenha limitações intrínsecas (mas os seres humanos são melhores?). Mas a ideia ainda é muito útil para auxiliar consideravelmente a criação de programas, mecanizando muitas etapas e verificando automaticamente a correção da geração do programa.

Está fortemente relacionado a um resultado na lógica, chamado de correspondência de Curry-Howard (ou isomorfismo), que mostra que programas de computador e provas matemáticas são muito semelhantes.

Portanto, a idéia é que o sistema leve a especificação do programa como um teorema a ser provado. No caso do seu exemplo, seria algo como (informalmente): "existe um conjunto de todos os números primos menores que 10".

Em seguida, você tentará provar esse teorema, e os sistemas existentes o ajudarão a fazer a prova, automatizando algumas partes, possivelmente toda a prova e garantindo que você nunca cometa erros.

A partir dessa prova, pode-se extrair um programa que realmente calcula a lista desejada de números primos que foram especificados inicialmente.

Vários sistemas foram desenvolvidos no passado para elucidar essas idéias. Um dos mais conhecidos foi o LCF de Robin Milner , que criou o idioma ML para esse fim. Um dos sistemas mais avançados atualmente é o Coq .

Existem exemplos totalmente elaborados, alguns deles bastante complexos. Você pode encontrar algumas no artigo a seguir , embora não seja uma leitura simples e exija conhecimentos avançados de lógica.

A resposta da pergunta: Sim, mas no momento da redação deste artigo, para a maioria dos programas não triviais, as especificações parecem tão difíceis de escrever e depurar quanto os programas.

Mais seriamente, a resposta do babou é boa, mas também vou sugerir verificar a área dos tipos dependentes. Há um livro bastante bom usando Coq (isenção de responsabilidade completa: escrita por um amigo meu), mas também há Epigram, Agda e Idris. Isabelle / HOL também vale a pena conferir.

Tudo isso é baseado no cálculo de construções. Se você quiser conhecer a base teórica, procure a teoria do tipo Martin-Löf. Existem algumas ótimas apresentações por aí.

Seguindo uma tangente aqui, os geradores de programas (ou seja, sistemas que fornecem uma descrição de alto nível de algo em alguma linguagem especial) estão sempre presentes. Qualquer compilador é um desses, assim como qualquer um dos muitos geradores de analisadores. Naquela época, os sistemas chamados "idiomas de terceira geração", que geravam (a maioria do) código de um aplicativo de negócios típico, dada uma descrição de alto nível e um catálogo de dados disponíveis, eram populares.

A programação lógica e, de maneira mais geral, a programação declarativa tomam como premissa exatamente o que você propõe: ou seja, a partir de uma especificação lógica, retorna um resultado que atenda a essa especificação.

Uma área que parece abordar especificamente o exemplo "números primos menores que 10" que você fornece é a Programação de Restrições, que tenta encontrar soluções para problemas que envolvem certas restrições, incluindo restrições de número inteiro como as que você forneceu.

Você pode tentar o ECLiPSe para uma implementação específica (de código aberto) desse sistema.