Existem linguagens prováveis ​​do mundo real?(escala?)

StackOverflow https://stackoverflow.com/questions/4065001

Pergunta

fui ensinado sobre sistemas formais na universidade, mas fiquei desapontado porque eles não pareciam ser usados ​​na palavra real.

Gosto da ideia de poder saber que algum código (objeto, função, qualquer que seja) funciona, não por meio de testes, mas por prova.

Tenho certeza de que estamos todos familiarizados com os paralelos que não existem entre a engenharia física e a engenharia de software (o aço se comporta de maneira previsível, o software pode fazer qualquer coisa - quem sabe!), e eu adoraria saber se existe alguma linguagem que pode ser usado na palavra real (é pedir muito um framework web?)

Ouvi coisas interessantes sobre a testabilidade de linguagens funcionais como scala.

Como software engenheiros que opções temos?

Foi útil?

Solução

Sim, existem linguagens projetadas para escrever software comprovadamente correto.Alguns são até usados ​​na indústria. Faísca Ada é provavelmente o exemplo mais proeminente.Conversei com algumas pessoas da Praxis Critical Systems Limited que o usaram para código executado em Boings (para monitoramento de mecanismo) e parece muito bom.(Aqui está um ótimo resumo/descrição do idioma.) Esta linguagem e o sistema de prova que o acompanha usam a segunda técnica descrita abaixo.Ele nem suporta alocação dinâmica de memória!

Minha impressão e experiência é que existem duas técnicas para escrever software correto:

  • Técnica 1:Escreva o software em uma linguagem com a qual você se sinta confortável (C, C++ ou Java, por exemplo).Pegue uma especificação formal dessa linguagem e prove que seu programa está correto.

    Se sua ambição é estar 100% correta (o que geralmente é um requisito na indústria automobilística/aeroespacial), você gastaria pouco tempo programando e mais tempo provando.

  • Técnica 2:Escreva o software em uma linguagem um pouco mais estranha (algum subconjunto de Ada ou versão aprimorada do OCaml, por exemplo) e escreva a prova de correção ao longo do caminho.Aqui a programação e a prova andam de mãos dadas.Programar em Coq os iguala completamente!(Veja o Correspondência Curry-Howard)

    Nestes cenários você sempre terá um programa correto.(É garantido que um bug esteja enraizado na especificação.) Você provavelmente gastará mais tempo programando, mas, por outro lado, estará provando que está correto ao longo do caminho.

Observe que ambas as abordagens dependem do fato de você ter uma especificação formal em mãos (de que outra forma você poderia dizer qual é o comportamento correto/incorreto) e uma semântica da linguagem formalmente definida (de que outra forma você seria capaz de dizer qual é o comportamento real? do seu programa é).

Aqui estão mais alguns exemplos de abordagens formais.Se é do "mundo real" ou não, depende de para quem você pergunta :-)

Eu conheço apenas um "provavelmente correto" linguagem de aplicação web: você.É garantido que um programa Ur que "passa pelo compilador" não:

  • Sofra qualquer tipo de ataque de injeção de código
  • Retornar HTML inválido
  • Contém links inativos dentro do aplicativo
  • Têm incompatibilidades entre os formulários HTML e os campos esperados pelos seus manipuladores
  • Inclui código do lado do cliente que faz suposições incorretas sobre os serviços de estilo "AJAX" que o servidor web remoto fornece
  • Tentativa de consultas SQL inválidas
  • Usar empacotamento ou desempacotamento inadequado na comunicação com bancos de dados SQL ou entre navegadores e servidores web

Outras dicas

Para responder a esta pergunta, você realmente precisa definir o que entende por “provável”.Como Ricky apontou, qualquer linguagem com um sistema de tipos é uma linguagem com um sistema de prova integrado que é executado toda vez que você compila seu programa.Esses sistemas de prova são quase sempre tristemente impotentes – respondendo a perguntas como String contra Int e evitar perguntas como "a lista está classificada?" – mas são sistemas de prova nenhuma.

Infelizmente, quanto mais sofisticados forem seus objetivos de prova, mais difícil será trabalhar com um sistema que possa verificar suas provas.Isso rapidamente se transforma em indecidibilidade quando você considera o tamanho da classe de problemas que são indecidíveis nas Máquinas de Turing.Claro, teoricamente você pode fazer coisas básicas, como provar a exatidão do seu algoritmo de classificação, mas qualquer coisa além disso será pisar em gelo muito fino.

Mesmo para provar algo simples como a exatidão de um algoritmo de classificação, é necessário um sistema de prova comparativamente sofisticado.(observação:como já estabelecemos que os sistemas de tipos são um sistema de prova embutido na linguagem, vou falar sobre as coisas em termos de teoria de tipos, em vez de acenar com as mãos ainda mais vigorosamente. Tenho quase certeza de que uma prova de correção completa na classificação de lista exigiria alguma forma de tipos dependentes; caso contrário, você não teria como fazer referência a valores relativos no nível do tipo.Isso imediatamente começa a invadir domínios da teoria dos tipos que se mostraram indecidíveis.Portanto, embora você possa provar a correção do seu algoritmo de classificação de lista, a única maneira de fazer isso seria usar um sistema que também lhe permitirá expressar provas que ele não pode verificar.Pessoalmente, acho isso muito desconcertante.

Há também o aspecto da facilidade de uso ao qual aludi anteriormente.Quanto mais sofisticado for o seu sistema de tipos, menos agradável será de usar.Essa não é uma regra rígida e rápida, mas acho que é válida na maior parte.E como acontece com qualquer sistema formal, você frequentemente descobrirá que expressar a prova é mais trabalhoso (e mais sujeito a erros) do que criar a implementação em primeiro lugar.

Com tudo isso resolvido, vale a pena notar que o sistema de tipos do Scala (como o de Haskell) é Turing Complete, o que significa que você pode teoricamente use-o para provar qualquer propriedade decidível sobre seu código, desde que você tenha escrito seu código de forma que ele seja passível de tais provas.Haskell é quase certamente uma linguagem melhor para isso do que Java (já que a programação em nível de tipo em Haskell é semelhante ao Prolog, enquanto a programação em nível de tipo em Scala é mais semelhante ao SML).Não aconselho que você use os sistemas de tipos Scala ou Haskell dessa maneira (provas formais de correção algorítmica), mas a opção está teoricamente disponível.

No geral, penso que a razão pela qual não vimos sistemas formais no “mundo real” decorre do facto de os sistemas formais de prova terem cedido à impiedosa tirania do pragmatismo.Como mencionei, há tanto esforço envolvido na elaboração de provas de correção que quase nunca vale a pena.A indústria decidiu há muito tempo que era mais fácil criar testes ad hoc do que passar por qualquer tipo de processo de raciocínio analítico formal.

As linguagens digitadas comprovam a ausência de certas categorias de falhas.Quanto mais avançado o sistema de tipos, mais falhas eles podem provar a ausência.

Para provar que todo um programa funciona, sim, você está ultrapassando os limites das linguagens comuns, onde matemática e programação se encontram, apertam as mãos e depois falam usando símbolos gregos sobre como os programadores não conseguem lidar com símbolos gregos.De qualquer maneira, isso é quase o Σ.

Você está fazendo uma pergunta que muitos de nós fizemos ao longo dos anos.Não sei se tenho uma boa resposta, mas aqui estão algumas peças:

  • Existem linguagens bem compreendidas com possibilidade de serem comprovadas em uso hoje;Lisp via ACL2 é um deles e, claro, Scheme também tem uma definição formal bem compreendida.

  • vários sistemas tentaram usar linguagens funcionais puras, ou quase puras, como Haskell.Existem muitos métodos formais que funcionam em Haskell.

  • Há mais de 20 anos, houve uma coisa de curta duração no uso da prova manual de uma linguagem formal que era então rigorosamente traduzida para uma linguagem compilada.Alguns exemplos foram Software Cleanroom da IBM, ACL, Gypsy e Rose out of Computational Logic, John McHugh e meu trabalho na compilação confiável de C, e meu próprio trabalho na prova manual para programação de sistemas C.Todos eles chamaram a atenção, mas nenhum deles colocou muito em prática.

Uma pergunta interessante a ser feita, penso eu, é: quais seriam as condições suficientes para colocar em prática abordagens formais?Eu adoraria ouvir algumas sugestões.

Você pode investigar linguagens puramente funcionais como Haskell, que são usados ​​quando um de seus requisitos é demonstrabilidade.

Esse é uma leitura divertida se você estiver interessado em linguagens de programação funcionais e linguagens de programação funcionais puras.

os usos no mundo real de tais linguagens prováveis ​​seriam incrivelmente difíceis de escrever e entender depois.o mundo dos negócios precisa de software funcional e rápido.

Linguagens "comprováveis" simplesmente não são dimensionadas para escrever/ler a base de código de um grande projeto e parecem funcionar apenas em casos de uso pequenos e isolados.

Estou envolvido em duas linguagens prováveis.A primeira é a linguagem suportada pelo Perfect Developer, um sistema para especificar software, refiná-lo e gerar código.Ele tem sido usado em alguns sistemas grandes, incluindo o próprio PD, e é ensinado em diversas universidades.A segunda linguagem demonstrável com a qual estou envolvido é um subconjunto demonstrável do MISRA-C, consulte Blog de verificação C/C++ para mais.

Confira Ómega.

Esse introdução contém uma implementação relativamente fácil de árvores AVL com prova de correção incluída.

Scala foi criado para ser o “mundo real”, portanto nenhum esforço foi feito para torná-lo comprovável.O que você pode fazer no Scala é produzir código funcional.O código funcional é muito mais fácil de testar, o que é IMHO um bom compromisso entre o "mundo real" e a comprovação.

EDITAR ===== Removidas minhas ideias incorretas sobre o ML ser "demonstrável".

Minha definição (controversa) de "mundo real" no contexto de código comprovadamente correto é:

  • Deve envolver algum grau de automação, caso contrário, você gastará muito tempo provando e lidando com pequenos detalhes confusos, e isso será totalmente impraticável (exceto, talvez, para software de controle de nave espacial e esse tipo de coisa, para o qual você pode realmente querer gastar megabucks em verificações meticulosas).
  • Deve suportar algum grau de programação funcional, que ajuda você a escrever código muito modular, reutilizável e mais fácil de raciocinar.Obviamente, a programação funcional não é necessária para escrever ou provar o Hello World, ou uma variedade de programas simples, mas a certa altura, a programação funcional se torna muito útil.
  • Embora você não precise necessariamente ser capaz de escrever seu código em uma linguagem de programação convencional, como alternativa, você deve pelo menos ser capaz de traduzir automaticamente seu código em um código razoavelmente eficiente escrito em uma linguagem de programação convencional, de maneira confiável. caminho.

Os requisitos acima são relativamente mais universais.Outros, como a capacidade de modelar código imperativo ou a capacidade de provar que funções de ordem superior estão corretas, podem ser importantes ou essenciais para algumas tarefas, mas não todas.

Em vista desses pontos, muitas das ferramentas listadas em esta minha postagem no blog podem ser úteis - embora sejam quase todos novos e experimentais ou desconhecidos para a grande maioria dos programadores da indústria.No entanto, existem algumas ferramentas muito maduras abordadas lá.

Que tal Idris e Agda?Mundo real o suficiente?

Como um bom exemplo da vida real, há um projeto que visa fornecer uma biblioteca HTTP REST verificada escrita em Agda, chamada Lemmachine: https://github.com/larrytheliquid/Lemmachine

Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top