O que sabemos sobre programas comprovadamente corretos?

A complexidade cada vez maior dos programas de computador e a posição cada vez mais crucial que os computadores têm em nossa sociedade me deixam pensando por que ainda não usamos coletivamente linguagens de programação nas quais você precisa dar uma prova formal de que seu código funciona corretamente.

Acredito que o termo seja um 'compilador de certificação' (o encontrei aqui ): um compilador que compila uma linguagem de programação na qual não apenas é necessário escrever o código, mas também declarar a especificação do código e provar que o código adere ao especificação (ou use um fornecedor automatizado para fazer isso).

Ao pesquisar na Internet, encontrei apenas projetos que usam uma linguagem de programação muito simples ou projetos com falha que tentam adaptar linguagens de programação modernas. Isso me leva à minha pergunta:

Existem compiladores de certificação implementando uma linguagem de programação completa ou isso é muito difícil / teoricamente impossível?

Além disso, ainda não vi nenhuma classe de complexidade que envolva programas comprováveis, como "a classe de todas as línguas decididas por uma máquina de Turing para a qual existe uma prova de que essa máquina de Turing pára", que chamarei de $ProvableR$ , como análogo a $R$ , o conjunto de linguagens recursivas.

Eu posso ver vantagens de estudar uma classe de complexidade: por exemplo, para $ProvableR$ o problema da parada é decidível (eu até conjecturo $ProvableRE$ definido da maneira óbvia. a maior classe de idiomas para a qual é decidível). Além disso, duvido que excluiríamos programas praticamente úteis: quem usaria um programa quando você não pode provar que ele termina?

Então, minha segunda pergunta é:

O que sabemos sobre classes de complexidade que exigem que suas linguagens contenham provadamente determinadas propriedades?

"Compilador de certificação" geralmente significa algo ligeiramente diferente: significa que você possui um compilador que pode provar que o código de máquina que ele emite implementa corretamente implementa a semântica de alto nível. Ou seja, é uma prova de que não há erros do compilador. Os programas que as pessoas fornecem ao compilador ainda podem estar errados, mas o compilador gerará uma versão correta do código da máquina do programa errado. A maior história de sucesso nesse sentido é o compilador verificado pelo CompCert , que é um compilador para um grande subconjunto de C.

O compilador Compcert em si é um programa com uma prova de correção (feita em Coq), que garante que, se gerar código para um programa, ele estará correto (com relação à semântica operacional de assembly & C que os designers do CompCert usaram). O esforço para verificar essas coisas pela máquina é bastante grande; normalmente, a prova de correção estará entre 1x e 100x o tamanho do programa que você está verificando. Escrever programas e provas verificados pela máquina é uma nova habilidade que você precisa aprender - não é matemática ou programação, como de costume, embora dependa de ser capaz de fazer as duas coisas bem. Parece que você está começando do zero, como se fosse um programador iniciante novamente.

Porém, não existem barreiras teóricas especiais. A única coisa nesse sentido é o teorema de Blum Size, que para qualquer idioma em que todos os programas são totais, é possível encontrar um programa em um idioma recursivo geral que será pelo menos exponencialmente maior quando programado no idioma total. A maneira de entender esse resultado é que um idioma total codifica não apenas um programa, mas também uma prova de término. Assim, você pode ter programas curtos com provas de término longas. No entanto, isso realmente não importa na prática, pois apenas escreveremos programas com provas de terminação gerenciáveis.

EDIT: Dai Le pediu alguma elaboração do último ponto.

Essa é principalmente uma afirmação pragmática, baseada no fato de que, se você pode entender por que um programa funciona, é improvável que o motivo seja alguns milhões de páginas invariáveis ​​e vastas. (Os invariantes mais longos que usei têm algumas páginas e, rapaz, eles fazem os revisores resmungarem! Compreensivelmente, também, uma vez que o invariante é a razão pela qual o programa trabalha despojado de toda a narrativa que ajuda as pessoas a entendê-lo.)

Mas também existem algumas razões teóricas. Basicamente, não sabemos muitas maneiras de inventar sistematicamente programas cujas provas de correção são muito longas. O método principal é (1) pegar a lógica na qual você prova a exatidão, (2) encontrar uma propriedade que não possa ser expressa diretamente nessa lógica (provas de consistência são a fonte típica) e (3) encontrar um programa cujo prova de correção depende de uma família de consequências expressáveis ​​da propriedade inexprimível. Como (2) é inexprimível, isso significa que a prova de cada conseqüência expressável deve ser feita independentemente, o que permite aumentar o tamanho da prova de correção. Como um exemplo simples, observe que na lógica de primeira ordem com uma relação pai, você não pode expressar a relação ancestral.$k$$k$) é expressável, para cada fixo . Portanto, ao fornecer um programa que usa alguma propriedade de ancestralidade até um certo nível (digamos, 100), você pode forçar uma prova de correção no FOL para conter provas dessas propriedades centenas de vezes.$k$

A abordagem sofisticada sobre esse assunto é chamada de "matemática reversa" e é o estudo de quais axiomas são necessários para provar os teoremas dados. Não sei muito sobre isso, mas se você postar uma pergunta sobre sua aplicação no CS, tenho certeza de que pelo menos Timothy Chow, e provavelmente várias outras pessoas, poderão lhe dizer coisas interessantes.

Eu acho que a resposta para a primeira pergunta é que geralmente é muito trabalho com as ferramentas atuais. Para entender, sugiro tentar provar a correção do Bubble Sort no Coq (ou se você preferir um pouco mais de desafio, use o Quick Sort). Não acho que seja razoável esperar que os programadores escrevam programas verificados, desde que provar que a correção de tais algoritmos básicos seja tão difícil e demorado.

Essa pergunta é semelhante a perguntar por que os matemáticos não escrevem provas formais verificáveis ​​por verificadores de provas? Escrever um programa com uma prova formal de correção significa provar um teorema matemático sobre o código escrito, e a resposta a essa pergunta também se aplica à sua pergunta.

Isso não significa que não houve casos de sucesso de programas verificados. Eu sei que existem grupos que estão provando a correção de sistemas como o hipervisor da Microsoft . Um caso relacionado é o Verified C Compiler da Microsoft . Mas, em geral, as ferramentas atuais precisam de muito desenvolvimento (incluindo seus aspectos SE e HCI) antes de se tornarem úteis para programadores gerais (e matemáticos).

Em relação ao parágrafo final da resposta de Neel sobre o crescimento do tamanho do programa para linguagens com apenas funções totais, é fácil provar ainda mais (se eu entendi direito). É razoável esperar que a sintaxe de qualquer linguagem de programação seja ce e o conjunto de funções computáveis ​​totais não seja ce; portanto, para qualquer linguagem de programação em que todos os programas sejam totais, há uma função computável total que não pode ser calculada por nenhum programa ( de qualquer tamanho) nesse idioma.

Para a segunda pergunta, eu respondi uma pergunta semelhante no blog de Scott há algum tempo. Basicamente, se a classe de complexidade tem uma boa caracterização e é representável computacionalmente (ou seja, é ce), podemos provar que alguma representação dos problemas na classe de complexidade é comprovadamente total em teorias muito fracas correspondentes à classe de complexidade. A idéia básica é que as funções comprovadamente totais da teoria contenham todas as funções e um problema que é A C $AC^0$$AC^0$-completo para a classe de complexidade, portanto, contém todos os problemas na classe de complexidade e pode provar a totalidade desses programas. A relação entre provas e teoria da complexidade é estudada na complexidade da prova; consulte o livro recente de SA Cook e P. Nguyen " Fundamentos lógicos da complexidade da prova ", se você estiver interessado. (Um rascunho de 2008 está disponível.) Portanto, a resposta básica é a de muitas classes "Provably C = C".

Isso não é verdade em geral, pois existem classes de complexidade semântica que não possuem caracterização sintática, por exemplo, funções computáveis ​​totais. Se por recursiva você quer dizer funções recursivas totais, então as duas não são iguais, e o conjunto de funções computáveis ​​que são comprovadamente totais em uma teoria é bem estudado na literatura da teoria da prova e é chamado de funções comprovadamente totais da teoria. Por exemplo: as funções comprovadamente totais de são £ 0 funções -recursive (ou equivalentemente funções no sistema de Gódel T ), as funções comprovadamente totais de P $PA$$\epsilon_0$$T$ são função no sistema de Girard F , as funções comprovadamente totais de$PA^2$$F$ são funções recursivas primitivas, ....$I\Sigma_1$

Mas não me parece que isso signifique muito no contexto de verificação de programas, pois também existem programas que estão computando extensionalmente a mesma função, mas não podemos provar que os dois programas estão computando a mesma função, ou seja, os programas são extensionalmente iguais, mas não intencionalmente. (Isso é semelhante à Estrela da Manhã e à Estrela da noite.) Além disso, é fácil modificar um determinado programa comprovadamente total para obter um programa que a teoria é incapaz de provar sua totalidade.

Eu acho que as duas perguntas estão relacionadas. O objetivo é obter um programa verificado. Um programa verificado significa que o programa atende a uma descrição, que é uma declaração matemática. Uma maneira é escrever um programa em uma linguagem de programação e, em seguida, provar suas propriedades como satisfaz a descrição, que é a prática mais comum. Outra opção é tentar provar a afirmação matemática que descreve o problema usando meios restritos e depois extrair um programa verificado. Por exemplo, se provarmos na teoria correspondente a que, para qualquer número dado n, existe uma sequência de números primos cujo produto é igual a n , podemos extrair um $P$$n$$n$$P$algoritmo para fatoração da prova. (Também existem pesquisadores que tentam automatizar a primeira abordagem o máximo possível, mas verificar propriedades interessantes não triviais dos programas é computacionalmente difícil e não pode ser completamente verificado sem falsos positivos e negativos.)

O que você está perguntando na primeira pergunta às vezes é chamado de "compilador de verificação" e, alguns anos atrás, Tony Hoare o oferecia como um grande desafio para a pesquisa em computação . Até certo ponto, isso já existe e está em uso ativo em ferramentas como o provador do teorema de Coq , que organiza o problema por meio da teoria dos tipos e do princípio das proposições como tipos (" Curry-Howard ").

Edição: só queria adicionar ênfase em "até certo ponto". Isso está longe de ser um problema resolvido, mas o sucesso da Coq dá esperança de que não seja um sonho.

Uma ferramenta que verifica se um programa está correto às vezes é chamada de verificador de programa. Nesse contexto, "correto" geralmente significa duas coisas: que o programa nunca produz certas saídas (pense em falha de segmentação, NullPointerException etc.) e que o programa concorda com uma especificação.

O código e a especificação podem concordar e ainda ser percebidos como incorretos. Em certo sentido, pedir aos desenvolvedores que escrevam especificações é como pedir a dois desenvolvedores que resolvam o problema. Se as duas implementações concordarem, você terá maior confiança de que elas estão OK. Em outro sentido, no entanto, as especificações são melhores que uma segunda implementação. Como a especificação não precisa ser eficiente ou mesmo executável, pode ser muito mais sucinta e, portanto, mais difícil de se errar.

Com essas advertências em mente, recomendo que você verifique o verificador do programa Spec # .

No caso geral, é impossível criar um algoritmo que confirme se um algoritmo é equivalente a uma especificação. Esta é uma prova informal:

Quase todas as linguagens de programação são completas em Turing. Portanto, qualquer idioma decidido por uma TM também pode ser decidido por um programa escrito nesse idioma.

$Equivalence/TM$ é indecidible. Como conseqüência da integridade de Turing, o mesmo vale para os programas do idioma especificado. Em outras palavras, é indecidível saber se as entradas que você deseja que seu programa aceite e as que ele realmente faz são as mesmas.

$Equivalence/TM$$Non-emptiness/TM$$Emptiness/TM$$Emptiness/TM$$Equivalence/TM$$Equivalence/TM$também é inaceitável. Portanto, você pode usar um algoritmo, independentemente de duas máquinas não serem equivalentes, mas não pode ter certeza se são equivalentes ou se não deu tempo suficiente ao seu algoritmo.

No entanto, isso é apenas para o caso geral. É possível que você decida se as especificações são equivalentes ou não ao programa, resolvendo uma versão mais relaxada do problema. Por exemplo, você pode examinar apenas várias entradas ou dizer que os dois programas são equivalentes a alguma incerteza. É disso que se trata o teste de software.

Quanto ao restante de suas perguntas:

Nota: Esta parte foi editada para esclarecimentos. Acontece que cometi o erro que estava tentando evitar, desculpe.

$TrueR$$TrueR \subseteq R$

$ProvableR = TrueR$$ProvableR \subset TrueR$$TrueR \subset ProvableR$$A \epsilon TrueR$$A$$A$$A \epsilon ProvableR$

Informalmente, isso pode ser resumido como: Você não sabe que um idioma é decidível até que você prove que é. Portanto, se em um sistema formal você tem o conhecimento de que um idioma é decidível, esse conhecimento também pode servir como prova disso. Portanto, você não pode ter simultaneamente o conhecimento de que um idioma é decidível e não pode ser provado, portanto, essas duas declarações são mutuamente exclusivas.

$R$$ProvableR$$ProvableR \subset R$$R$

@Kaveh resume melhor: Provable sempre significa provable em algum sistema / teoria e não coincide com a verdade em geral.

O mesmo vale para qualquer outra classe de complexidade: para determinar a associação, você precisa primeiro de uma prova. É por isso que acredito que sua segunda pergunta é muito geral, pois contém não apenas a teoria da complexidade, mas também a teoria da computação, dependendo da propriedade que você deseja que a linguagem tenha.

A seguinte monografia clássica estuda quase exatamente sua segunda pergunta:

Hartmanis, J. Computações viáveis ​​e propriedades de complexidade comprovável , Série de Conferências Regionais CBMS-NSF em Matemática Aplicada, 30. Sociedade de Matemática Industrial e Aplicada (SIAM), Filadélfia, Pa., 1978.

$\{L(M_i) | T_i(n) \leq T(n) \text{ is provable in F}\}$$M_i$$T_i(n)$$M_i$$n$

$T(n) \geq n \log(n)$$g(n) \geq 1$$F$$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$

$T(n)$$F$$TIME[T(n)] \neq TIME[T(n)]$ .

$T(n) \geq n \log(n)$$TIME[T(n)] = \{ L(M_i) | \text{F proves} (\exists j)[L(M_j) = L(M_i) \wedge T_j(n) \leq T(n)] \}$

Para o espaço, no entanto, a situação é melhor controlada:

$s(n) \geq n$$SPACE[s(n)] = F$$SPACE[s(n)]$ .

$SPACE[S(n)]=F$$SPACE[S(n)]$$S(n) \geq n$$s(n)$$SPACE[S(n)]=SPACE[s(n)]$

A questão deve ser colocada corretamente. Por exemplo, ninguém nunca quer saber se um programa real seria concluído com memória infinita e alguns meios de acessá-lo (talvez uma operação para mover o endereço base por algum número). O teorema de Turing é irrelevante para programar a correção em qualquer sentido concreto, e as pessoas que o citam como barreira à verificação do programa estão confundindo duas coisas bem diferentes. Quando engenheiros / programadores falam sobre a correção do programa, eles querem saber sobre propriedades finitas. Isso também é verdade para os matemáticos que estão interessados ​​em saber se algo é provável. A carta de Godel http://vyodaiken.com/2009/08/28/godels-lost-letter/ explica isso em alguns detalhes.

Nomeadamente, isso obviamente significaria que, apesar da indecidibilidade do problema de Entscheidung, o trabalho mental de um matemático sobre questões do tipo sim ou não poderia ser completamente substituído por uma máquina. Afinal, basta escolher o número natural n tão grande que, quando a máquina não produz um resultado, não faz sentido pensar mais sobre o problema.

Pode ser inviável examinar o imenso conjunto de estados de um programa em execução em um computador real e detectar estados ruins; não há razão teórica para que isso não possa ser feito. De fato, houve muito progresso nesse campo - por exemplo, consulte http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf (obrigado a Neil Immerman por me falando sobre isso)

Um problema diferente e mais difícil é especificar exatamente quais propriedades se deseja que um programa tenha para estar correto.