Ótimo texto. Pela minha experiência anterior com verificação de programas, Rust parece ser a linguagem moderna mais útil para aplicar métodos formais
As regras de Rust eliminam muitos casos difíceis de formalizar. O grande problema restante é a análise de deadlocks do ponto de vista de threads e do ponto de vista de Rc/empréstimos; os dois são, em certa medida, equivalentes. Se Rust tivesse análise estática de deadlocks, parece que até ponteiros de desreferenciação seguros seriam possíveis, e, se fosse possível provar que todas as chamadas de borrow/upgrade não falham, daria para eliminar a maior parte da contagem de referências. Com isso, quando possível, a mutabilidade interna também viria de graça
O grande problema dos provadores de teoremas é que, como são feitos por pessoas que gostam de provar teoremas, acabam caindo no formalismo e ficando desalinhados com programadores e com uma boa noção de UI. A maioria das obrigações de prova pode ser tratada por solvers SAT, mas problemas difíceis exigem ferramentas mais pesadas. Coq é manual demais, e o autor considera ACL2 funcional demais. Aprendizado de máquina pode ajudar a orientar provadores de teoremas. É difícil confiar a prova em si a ele, mas parece possível inferir planos de prova em código cujo fluxo de controle e uso de dados sejam, em geral, semelhantes
F* é quase uma linguagem mítica que prova tudo automaticamente. Ela usa um solver SMT mais forte que SAT e, quando a resolução automática falha, também permite provas manuais
As rotinas criptográficas do Firefox e do Wireguard não foram escritas em Rust, mas em F*; mais precisamente, em Low*, uma DSL de baixo nível embutida em F*, e são totalmente verificadas https://project-everest.github.io/ https://mitls.org/
Concordo, mas acho que Lean, graças aos seus ricos recursos de metaprogramação, está avançando muito na experiência de usuário da verificação interativa de provas de teoremas
O problema ao aplicar esse tipo de ferramenta à verificação de uma linguagem externa como Rust é que as provas não são escritas na linguagem-alvo, então o desenvolvedor precisa aprender duas linguagens. Com base na experiência de escrever Creusot, no trabalho com Verus e Aeneas e na experiência no laboratório Why3, venho pensando em como seria um “Rust consciente de verificação”. Se uma linguagem assim fosse criada desde o início, sua verificabilidade poderia melhorar em etapas até em relação a Rust, e acho que isso teria um efeito especialmente grande nas partes difíceis das provas
Acho que a família Coq/Agda/Lean deve acabar vencendo no campo das provas. A interação é um modelo bem bom para um ciclo de feedback, e esses sistemas já existem e funcionam de verdade
O recurso embutido de que mais sinto falta é algo equivalente a “rode quickcheck na minha prova”. Quando há código e você tenta provar uma propriedade que não é verdadeira, é fácil ficar arrancando os cabelos sem entender por que a prova não fecha. Se, no meio de uma prova, você chega a um estado que não faz sentido, seria bom ter um comando como “gere um contraexemplo aqui” e ele cuspir um contraexemplo. Provas são muito dependentes do caminho e, em geral, não são fáceis, mas essas ferramentas parecem estar muito perto da grandeza. O processo de tentar provar código também precisa refletir a possibilidade de que esse código tenha bugs
A ideia de aprendizado de máquina orientar provadores de teoremas é interessante. Se o sistema de aprendizado de máquina estiver certo, ele leva a uma prova válida e traz um grande ganho; se estiver errado, não há grande prejuízo
O provador não deriva uma prova incorreta; ele simplesmente deixa de derivar uma prova válida. Acho que não há muitas aplicações de aprendizado de máquina com essa propriedade
Não sou especialista em verificação formal, mas acho que locks, no sentido tradicional, não ajudam muito. Nenhum compilador oferece algo realmente útil sobre locks; você simplesmente aceita o risco e convive com ele
Na verdade, em Rust, locks e contagem de referências são estruturas de runtime. Arc quebra bastante o modelo RAII de Rust, a ponto de terem precisado remover scoped threads, cujos destrutores tinham de ser executados antes do fim do escopo. Contagem de referências global tem problemas de ciclos e vazamentos, e volta a ser um problema global. Talvez seja difícil eliminá-la por completo, mas acredito que é melhor confiná-la em escopos no estilo arena. Para locks, parece ser necessário algo como estruturas de dados assimétricas, como canais. Em Go, canais são separados em remetente e receptor, e é possível colocar defer close(ch) na goroutine remetente; mesmo em caso de pânico, sua execução é garantida quando o restante da thread termina. Não precisa necessariamente ser um canal, mas separar os papéis de leitura-escrita/produtor-consumidor torna o raciocínio muito mais fácil e deve ajudar também na análise formal
Gosto de como isso começou com uma citação de um artigo de Hoare de por volta de 1973 e agora já chegou ao segundo texto. No thread do HN do texto original de boat, deixei um comentário longo dizendo que, embora seja compreensível, dado o contexto de boat, inclinar aquela citação para uma perspectiva centrada em Rust estreita artificialmente o escopo da crítica de Hoare
Agora Grayson tomou esse recorte estreito como ponto de partida para discutir algumas áreas e pontos de design interessantes de Rust. Ainda acho que meu comentário estava correto, mas a discussão que surgiu a partir do texto de Grayson foi suficiente para compensar minhas objeções técnicas ao texto que serviu de ponto de partida
Por volta de meados dos anos 1990, o próprio Hoare já havia percebido que poderia haver algo errado nos fundamentos da abordagem centrada em solidez dos anos 1970: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Depois disso, com o surgimento de técnicas não sólidas mais avançadas do que testes simples, vejo que os métodos não sólidos passaram a ficar à frente dos métodos sólidos
1973 foi há 50 anos, a duração de uma vida profissional. Hoare chegou realmente perto
Ele identificou o problema e, em retrospecto, a solução de impor compartilhamento XOR mutabilidade por meio do sistema de tipos parece um pequeno passo. Se tivessem percebido naquela época que esse pequeno passo era a solução, teriam reduzido 50 anos de sofrimento enorme
O que eu havia escrito originalmente sobre a citação do artigo de Hoare feita por boat foi isto. Depois da primeira citação de Hoare e de uma breve introdução, o autor diz que “quando Tony Hoare disse que referências são como jumps, ele estava tratando do problema de estado mutável e com aliases”. Como withoutboats é um desenvolvedor famoso de Rust, essa interpretação não surpreende
Mas a própria citação não me parece reforçar essa perspectiva. Dá para ver isso como uma tentativa de pegar um lamento mais geral de Hoare sobre a própria existência semântica de referências e aplicá-lo ao modelo de estado mutável sem aliases de Rust para contornar o problema. Só que isso se parece mais com corrigir um recorte estreito de um problema maior e dizer que o problema inteiro desapareceu. As partes que ficaram de fora, especialmente o início da seção “Variables” e o exemplo de ALGOL 68, apontam com muito mais força para a ideia de que Hoare criticava não apenas estado mutável, mas o próprio conceito semântico de referência. Reconheço que Rust é uma tentativa de domar parte do problema, mas não vejo nenhuma linguagem como tendo “corrigido” esse problema
Não entendo muito bem por que há tantos elogios a este texto. Parece que ele cobre vários campos de análise de programas em um único parágrafo. Gosto do Graydon e respeito sua perspectiva, mas esse parágrafo é simplificado demais
A explicação de que linguagens com GC não se preocuparam em ter suporte forte a raciocínio local é um espantalho. Houve linguagens como Pony que usam GC e ainda assim colocam regiões no sistema de tipos. Além disso, há campos inteiros de análise de ponteiros e análise de escape, que inferem unicidade e determinam se duas referências podem ser aliases. O núcleo da tipagem estática também é dividir o heap em partes que não são aliases entre si por meio das técnicas de classes e campos. Não estamos falando de JavaScript, e não se deve fingir que Java/C#/Scala e inúmeras linguagens com GC não têm raciocínio local sobre estado mutável
No caso geral, não dá para fazer isso de forma totalmente automática, e na prática é preciso algo bem parecido com lógica de separação. A semântica do borrow checker de Rust também pode ser vista como uma espécie de lógica de separação simplificada
Classes e campos não fornecem raciocínio local completo sobre estado mutável. Isso porque uma classe/objeto A pode acabar dependendo do estado mutável de uma classe/objeto B. A herança de classes no estilo Java acrescenta por si só ainda mais complexidade à medida que o programa evolui com o tempo
Graydon não disse que GC torna impossível um raciocínio local forte. Ele está dizendo que, seja qual for o motivo, a maioria dos projetistas de linguagens fez escolhas contrárias a esse objetivo, e isso parece claramente verdadeiro
Claro que há contraexemplos, mas olhando para linguagens GC de uso geral e mainstream como Java, C# e Python, a afirmação está correta. É possível interpretar que a ideia original de orientação a objetos era mais próxima do modelo de atores atual, tentando alterar estruturas de dados possuídas apenas por passagem de mensagens. Mas as implementações reais de orientação a objetos quase não se aproximam desse objetivo. Java não impede que referências mutáveis ao mesmo objeto sejam armazenadas em vários objetos. Este texto explica melhor esse ponto: https://without.boats/blog/references-are-like-jumps/
Um quiz simples: o que este código imprime? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Edição: li errado a dupla negação. Mesmo relendo, ainda fico confuso. A ideia é que Java, ao contrário de JavaScript, tem raciocínio local?
Em geral gosto dos textos do Graydon, mas este, como muitos textos sobre técnicas formais, pode levar leitores que não conhecem a área a interpretações equivocadas. É parecido com dizer que o método para transformar chumbo em ouro melhorou em uma ordem de grandeza, sem dizer que ainda faltam mais 29 ordens de grandeza para chegar a uma relação custo-benefício prática A ausência de aliasing facilita muito a verificação formal? Sim. Isso significa que podemos verificar programas reais de forma prática e com bom custo-benefício? De jeito nenhum. Há programas, circuitos e componentes verificados formalmente todos os dias, mas eles são mais a exceção, são relativamente muito pequenos e feitos de uma maneira especialmente cuidadosa. Propriedades que ajudam no raciocínio local são importantes, mas não mudam substancialmente a forma de garantir, de maneira sólida, a correção de software mainstream
Mesmo programas em uma linguagem longe de ser Turing-completa — sem heap, sem ponteiros, sem inteiros, apenas variáveis booleanas e com loops que não podem executar mais de duas vezes — não são verificáveis na prática, porque se reduzem a TQBF. Para algumas propriedades, como segurança de memória, isso é possível, mas não é suficiente para o que o software precisa. Nas décadas de 1970 a 1990, havia a esperança de que, mesmo que a complexidade no pior caso fosse intratável, as garantias locais e a estrutura da linguagem nos afastariam desse pior caso; depois ficou demonstrado que não. A esperança de que os programas que as pessoas realmente escrevem estejam suficientemente longe do pior caso para permitir boas heurísticas também parece já não se sustentar
Há uma apresentação sobre esse tema: https://pron.github.io/posts/correctness-and-complexity
O resultado central é que a maioria das propriedades interessantes que queremos verificar não é composicional. Mesmo que se prove uma propriedade para cada componente P1...Pn, o custo de provar essa propriedade para P1 ○ ... ○ Pn não cresce apenas de forma superpolinomial em relação a n, mas também de forma superpolinomial em relação ao tamanho de cada componente. Ou seja, é tão difícil quanto se não tivéssemos dividido, e a correção não se decompõe. Por isso, “é possível verificar bastante coisa” e “o que é verificável é uma gota no oceano” podem ser ambos verdadeiros, e essa lacuna muitas vezes fica de fora nas discussões sobre técnicas formais
Venho repetindo o mesmo argumento centenas de vezes no HN há mais de 6 anos e, mesmo depois de muitos comentários que recebi nesse período, quase nenhum nuance foi acrescentado
Não está completamente errado, mas também não está completamente certo. É surpreendente que, apesar de muitas pessoas interessadas nesse tema terem tido centenas de oportunidades de mostrar isso ao longo dessas repetições, a posição não tenha evoluído em nada. Essa atitude soa como uma espécie de fechamento patológico e acaba desperdiçando o tempo de todos os que participam da conversa
Vejo o foco em solidez mais como algo que desvia a atenção de técnicas que, na prática, tiveram resultados melhores, do que como algo que ajude o objetivo de produzir software mais correto. Há técnicas práticas também sustentadas teoricamente, que às vezes surpreendem até quem achava que a solidez era o único caminho: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Isso se repete. Enquanto métodos sólidos recebem melhorias importantes, métodos não sólidos têm produzido, na prática, avanços muito maiores rumo a software mais correto. Um exemplo bem recente é https://antithesis.com. Claro que, em determinados contextos, técnicas sólidas podem ser mais poderosas e práticas, então é um tema complexo
É razoável esperar que pequenas bibliotecas em Rust possam ser verificadas quanto ao uso correto de unsafe. Só isso já seria realmente útil
Acabei de deixar um comentário relacionado também no texto sobre F*. Olhando apenas para a sintaxe, subjetivamente prefiro F*/F# a Rust, mas para o software de controle de shows que estou desenvolvendo decidi usar Ada/SPARK2014
Para que Rust atraia o mesmo tipo de pessoas que Ada/SPARK2014, precisa de um padrão oficial publicado, como linguagens estabelecidas como C, Common Lisp, Prolog, Fortran e COBOL. A AdaCore e a Ferrous Systems estão colaborando para oferecer ferramentas de verificação formal para Rust, como em Ada/SPARK2014, então Rust também está entrando nesse espaço, mas ainda não há um padrão publicado, e o legado de Ada e SPARK2014 é muito grande
É interessante ver a contagem de referências como uma espécie de GC otimizado de execução imediata, que funciona quando é usada estritamente em dados acíclicos ou quando se pode aceitar vazamentos cíclicos. Python usa a abordagem híbrida de contagem de referências + rastreamento descrita no texto, e já vi implantações em produção que forçavam o coletor por rastreamento a rodar apenas uma vez a cada N requisições
Perl usa contagem de referências pura, mas tem referências fracas, o que permite tornar os dados acíclicos do ponto de vista da contagem de referências, ao custo de se preocupar com quais partes de uma estrutura cíclica mantêm as referências. Koka, em teoria, usa contagem de referências, mas na prática tenta puxar o máximo possível para o tempo de compilação; se em y = x + 1 houver garantia de que x tem apenas uma referência e não será usado depois, ele pode reutilizar o mesmo armazenamento em y e fazer a alteração in-place
Nim oferece ORC, que combina contagem automática de referências com uma implementação do algoritmo Recycler de Bacon+Rajan. Esse algoritmo foi projetado para coletar apenas ciclos em sistemas baseados em contagem de referências, por isso é bastante rápido. Voltando ao Rust, há uma implementação stop-the-world do Recycler aqui: https://github.com/fitzgen/bacon-rajan-cc e ela é distribuída como o crate bacon-rajan-ccc neste fork: https://github.com/mbartlett21/bacon-rajan-cc A seção Alternatives do README traz links para outros experimentos na mesma área. Se estiver difícil encontrar o artigo do Recycler, reuni cópias em https://trout.me.uk/gc/, e, se você tiver gostos parecidos, também pode gostar dos artigos em https://trout.me.uk/lisp/
O Firefox também usa contagem de referências junto com um coletor de ciclos baseado em trial deletion para gerenciar ciclos entre objetos DOM em C++ e JS. Na verdade, Graydon ficou responsável pela implementação inicial
Sinto certa impaciência com a verificação formal de programas. Provar que um programa implementa corretamente uma especificação é teoricamente interessante, mas tem pouca utilidade prática
Escrever uma especificação correta é tão difícil quanto programar corretamente, então o problema difícil não é resolvido, apenas transferido. Há usos práticos para métodos formais, mas é raro encontrá-los
Isso é verdade para uma especificação completa, mas esse não é o objetivo real. Em geral, o que se quer provar são algumas propriedades essenciais. Por exemplo, que esta função sempre termina, ou que aquela função sempre retorna um array ordenado
Uma vez que se consegue fazer isso, é possível impor como pré-condição. Por exemplo, exigir que se mostre que um array já está ordenado antes de passá-lo para determinada função
Foi escrito em 15 de maio de 2024, dia em que o Rust 1.0 completava 9 anos
Li o texto linkado do Boats e achei excelente. Fiquei surpreso que a citação de Hoare de 50 anos atrás ainda seja relevante, e que também seja tão bem formulada
Eu gostaria que fosse possível usar algo mais simples, como type guards em tempo de compilação. Quando os trait bounds proliferam, programas em nível de tipos ficam difíceis de ler
Por exemplo, coisas como Where <<::Output as G>::Output as H>::Output: HList + Z ou type Output = <<::Output as G>::Output as H>::Output;. Aí você coloca Cons>>> nisso e percebe que números como o U8 do TypeNum também são, internamente, um aninhamento de Cons>>. Dá para avançar nessa área e fazer as verificações desejadas, mas as mensagens de erro podem se afastar bastante da forma como desenvolvedores humanos escrevem código, e a implementação também é muito dolorosa
A experiência do desenvolvedor é surpreendente porque isso não é “apenas uma função”, e sim uma combinação de genéricos específicos com tipos associados. Eu queria usar verificações em estilo runtime, mas executadas em tempo de compilação; para isso, porém, precisei escrever um código bem diferente. No fim, tornar o Rust em tempo de compilação em nível de tipos mais simples, funcional e legível talvez seja o caminho para que projetos desse tipo de análise formal ofereçam uma boa experiência a mantenedores e usuários. Em resumo, quero comptime em Rust. E também me pergunto se Future baseado em Pin<&mut Self> já está cristalizado. Gostaria de experimentar outras implementações internas de async/await, mas não sei por onde começar
1 comentários
Comentários do Hacker News
Ótimo texto. Pela minha experiência anterior com verificação de programas, Rust parece ser a linguagem moderna mais útil para aplicar métodos formais
As regras de Rust eliminam muitos casos difíceis de formalizar. O grande problema restante é a análise de deadlocks do ponto de vista de threads e do ponto de vista de
Rc/empréstimos; os dois são, em certa medida, equivalentes. Se Rust tivesse análise estática de deadlocks, parece que até ponteiros de desreferenciação seguros seriam possíveis, e, se fosse possível provar que todas as chamadas de borrow/upgrade não falham, daria para eliminar a maior parte da contagem de referências. Com isso, quando possível, a mutabilidade interna também viria de graçaO grande problema dos provadores de teoremas é que, como são feitos por pessoas que gostam de provar teoremas, acabam caindo no formalismo e ficando desalinhados com programadores e com uma boa noção de UI. A maioria das obrigações de prova pode ser tratada por solvers SAT, mas problemas difíceis exigem ferramentas mais pesadas. Coq é manual demais, e o autor considera ACL2 funcional demais. Aprendizado de máquina pode ajudar a orientar provadores de teoremas. É difícil confiar a prova em si a ele, mas parece possível inferir planos de prova em código cujo fluxo de controle e uso de dados sejam, em geral, semelhantes
As rotinas criptográficas do Firefox e do Wireguard não foram escritas em Rust, mas em F*; mais precisamente, em Low*, uma DSL de baixo nível embutida em F*, e são totalmente verificadas
https://project-everest.github.io/
https://mitls.org/
O problema ao aplicar esse tipo de ferramenta à verificação de uma linguagem externa como Rust é que as provas não são escritas na linguagem-alvo, então o desenvolvedor precisa aprender duas linguagens. Com base na experiência de escrever Creusot, no trabalho com Verus e Aeneas e na experiência no laboratório Why3, venho pensando em como seria um “Rust consciente de verificação”. Se uma linguagem assim fosse criada desde o início, sua verificabilidade poderia melhorar em etapas até em relação a Rust, e acho que isso teria um efeito especialmente grande nas partes difíceis das provas
O recurso embutido de que mais sinto falta é algo equivalente a “rode quickcheck na minha prova”. Quando há código e você tenta provar uma propriedade que não é verdadeira, é fácil ficar arrancando os cabelos sem entender por que a prova não fecha. Se, no meio de uma prova, você chega a um estado que não faz sentido, seria bom ter um comando como “gere um contraexemplo aqui” e ele cuspir um contraexemplo. Provas são muito dependentes do caminho e, em geral, não são fáceis, mas essas ferramentas parecem estar muito perto da grandeza. O processo de tentar provar código também precisa refletir a possibilidade de que esse código tenha bugs
O provador não deriva uma prova incorreta; ele simplesmente deixa de derivar uma prova válida. Acho que não há muitas aplicações de aprendizado de máquina com essa propriedade
Na verdade, em Rust, locks e contagem de referências são estruturas de runtime.
Arcquebra bastante o modelo RAII de Rust, a ponto de terem precisado remover scoped threads, cujos destrutores tinham de ser executados antes do fim do escopo. Contagem de referências global tem problemas de ciclos e vazamentos, e volta a ser um problema global. Talvez seja difícil eliminá-la por completo, mas acredito que é melhor confiná-la em escopos no estilo arena. Para locks, parece ser necessário algo como estruturas de dados assimétricas, como canais. Em Go, canais são separados em remetente e receptor, e é possível colocardefer close(ch)na goroutine remetente; mesmo em caso de pânico, sua execução é garantida quando o restante da thread termina. Não precisa necessariamente ser um canal, mas separar os papéis de leitura-escrita/produtor-consumidor torna o raciocínio muito mais fácil e deve ajudar também na análise formalGosto de como isso começou com uma citação de um artigo de Hoare de por volta de 1973 e agora já chegou ao segundo texto. No thread do HN do texto original de boat, deixei um comentário longo dizendo que, embora seja compreensível, dado o contexto de boat, inclinar aquela citação para uma perspectiva centrada em Rust estreita artificialmente o escopo da crítica de Hoare
Agora Grayson tomou esse recorte estreito como ponto de partida para discutir algumas áreas e pontos de design interessantes de Rust. Ainda acho que meu comentário estava correto, mas a discussão que surgiu a partir do texto de Grayson foi suficiente para compensar minhas objeções técnicas ao texto que serviu de ponto de partida
Depois disso, com o surgimento de técnicas não sólidas mais avançadas do que testes simples, vejo que os métodos não sólidos passaram a ficar à frente dos métodos sólidos
Ele identificou o problema e, em retrospecto, a solução de impor compartilhamento XOR mutabilidade por meio do sistema de tipos parece um pequeno passo. Se tivessem percebido naquela época que esse pequeno passo era a solução, teriam reduzido 50 anos de sofrimento enorme
Mas a própria citação não me parece reforçar essa perspectiva. Dá para ver isso como uma tentativa de pegar um lamento mais geral de Hoare sobre a própria existência semântica de referências e aplicá-lo ao modelo de estado mutável sem aliases de Rust para contornar o problema. Só que isso se parece mais com corrigir um recorte estreito de um problema maior e dizer que o problema inteiro desapareceu. As partes que ficaram de fora, especialmente o início da seção “Variables” e o exemplo de ALGOL 68, apontam com muito mais força para a ideia de que Hoare criticava não apenas estado mutável, mas o próprio conceito semântico de referência. Reconheço que Rust é uma tentativa de domar parte do problema, mas não vejo nenhuma linguagem como tendo “corrigido” esse problema
Não entendo muito bem por que há tantos elogios a este texto. Parece que ele cobre vários campos de análise de programas em um único parágrafo. Gosto do Graydon e respeito sua perspectiva, mas esse parágrafo é simplificado demais
A explicação de que linguagens com GC não se preocuparam em ter suporte forte a raciocínio local é um espantalho. Houve linguagens como Pony que usam GC e ainda assim colocam regiões no sistema de tipos. Além disso, há campos inteiros de análise de ponteiros e análise de escape, que inferem unicidade e determinam se duas referências podem ser aliases. O núcleo da tipagem estática também é dividir o heap em partes que não são aliases entre si por meio das técnicas de classes e campos. Não estamos falando de JavaScript, e não se deve fingir que Java/C#/Scala e inúmeras linguagens com GC não têm raciocínio local sobre estado mutável
Classes e campos não fornecem raciocínio local completo sobre estado mutável. Isso porque uma classe/objeto A pode acabar dependendo do estado mutável de uma classe/objeto B. A herança de classes no estilo Java acrescenta por si só ainda mais complexidade à medida que o programa evolui com o tempo
Claro que há contraexemplos, mas olhando para linguagens GC de uso geral e mainstream como Java, C# e Python, a afirmação está correta. É possível interpretar que a ideia original de orientação a objetos era mais próxima do modelo de atores atual, tentando alterar estruturas de dados possuídas apenas por passagem de mensagens. Mas as implementações reais de orientação a objetos quase não se aproximam desse objetivo. Java não impede que referências mutáveis ao mesmo objeto sejam armazenadas em vários objetos. Este texto explica melhor esse ponto: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Edição: li errado a dupla negação. Mesmo relendo, ainda fico confuso. A ideia é que Java, ao contrário de JavaScript, tem raciocínio local?
Em geral gosto dos textos do Graydon, mas este, como muitos textos sobre técnicas formais, pode levar leitores que não conhecem a área a interpretações equivocadas. É parecido com dizer que o método para transformar chumbo em ouro melhorou em uma ordem de grandeza, sem dizer que ainda faltam mais 29 ordens de grandeza para chegar a uma relação custo-benefício prática
A ausência de aliasing facilita muito a verificação formal? Sim. Isso significa que podemos verificar programas reais de forma prática e com bom custo-benefício? De jeito nenhum. Há programas, circuitos e componentes verificados formalmente todos os dias, mas eles são mais a exceção, são relativamente muito pequenos e feitos de uma maneira especialmente cuidadosa. Propriedades que ajudam no raciocínio local são importantes, mas não mudam substancialmente a forma de garantir, de maneira sólida, a correção de software mainstream
Mesmo programas em uma linguagem longe de ser Turing-completa — sem heap, sem ponteiros, sem inteiros, apenas variáveis booleanas e com loops que não podem executar mais de duas vezes — não são verificáveis na prática, porque se reduzem a TQBF. Para algumas propriedades, como segurança de memória, isso é possível, mas não é suficiente para o que o software precisa. Nas décadas de 1970 a 1990, havia a esperança de que, mesmo que a complexidade no pior caso fosse intratável, as garantias locais e a estrutura da linguagem nos afastariam desse pior caso; depois ficou demonstrado que não. A esperança de que os programas que as pessoas realmente escrevem estejam suficientemente longe do pior caso para permitir boas heurísticas também parece já não se sustentar
Há uma apresentação sobre esse tema: https://pron.github.io/posts/correctness-and-complexity
O resultado central é que a maioria das propriedades interessantes que queremos verificar não é composicional. Mesmo que se prove uma propriedade para cada componente P1...Pn, o custo de provar essa propriedade para P1 ○ ... ○ Pn não cresce apenas de forma superpolinomial em relação a n, mas também de forma superpolinomial em relação ao tamanho de cada componente. Ou seja, é tão difícil quanto se não tivéssemos dividido, e a correção não se decompõe. Por isso, “é possível verificar bastante coisa” e “o que é verificável é uma gota no oceano” podem ser ambos verdadeiros, e essa lacuna muitas vezes fica de fora nas discussões sobre técnicas formais
Não está completamente errado, mas também não está completamente certo. É surpreendente que, apesar de muitas pessoas interessadas nesse tema terem tido centenas de oportunidades de mostrar isso ao longo dessas repetições, a posição não tenha evoluído em nada. Essa atitude soa como uma espécie de fechamento patológico e acaba desperdiçando o tempo de todos os que participam da conversa
Isso se repete. Enquanto métodos sólidos recebem melhorias importantes, métodos não sólidos têm produzido, na prática, avanços muito maiores rumo a software mais correto. Um exemplo bem recente é https://antithesis.com. Claro que, em determinados contextos, técnicas sólidas podem ser mais poderosas e práticas, então é um tema complexo
unsafe. Só isso já seria realmente útilAcabei de deixar um comentário relacionado também no texto sobre F*. Olhando apenas para a sintaxe, subjetivamente prefiro F*/F# a Rust, mas para o software de controle de shows que estou desenvolvendo decidi usar Ada/SPARK2014
Para que Rust atraia o mesmo tipo de pessoas que Ada/SPARK2014, precisa de um padrão oficial publicado, como linguagens estabelecidas como C, Common Lisp, Prolog, Fortran e COBOL. A AdaCore e a Ferrous Systems estão colaborando para oferecer ferramentas de verificação formal para Rust, como em Ada/SPARK2014, então Rust também está entrando nesse espaço, mas ainda não há um padrão publicado, e o legado de Ada e SPARK2014 é muito grande
É interessante ver a contagem de referências como uma espécie de GC otimizado de execução imediata, que funciona quando é usada estritamente em dados acíclicos ou quando se pode aceitar vazamentos cíclicos. Python usa a abordagem híbrida de contagem de referências + rastreamento descrita no texto, e já vi implantações em produção que forçavam o coletor por rastreamento a rodar apenas uma vez a cada N requisições
Perl usa contagem de referências pura, mas tem referências fracas, o que permite tornar os dados acíclicos do ponto de vista da contagem de referências, ao custo de se preocupar com quais partes de uma estrutura cíclica mantêm as referências. Koka, em teoria, usa contagem de referências, mas na prática tenta puxar o máximo possível para o tempo de compilação; se em
y = x + 1houver garantia de quextem apenas uma referência e não será usado depois, ele pode reutilizar o mesmo armazenamento emye fazer a alteração in-placeNim oferece ORC, que combina contagem automática de referências com uma implementação do algoritmo Recycler de Bacon+Rajan. Esse algoritmo foi projetado para coletar apenas ciclos em sistemas baseados em contagem de referências, por isso é bastante rápido. Voltando ao Rust, há uma implementação stop-the-world do Recycler aqui: https://github.com/fitzgen/bacon-rajan-cc e ela é distribuída como o crate bacon-rajan-ccc neste fork: https://github.com/mbartlett21/bacon-rajan-cc A seção Alternatives do README traz links para outros experimentos na mesma área. Se estiver difícil encontrar o artigo do Recycler, reuni cópias em https://trout.me.uk/gc/, e, se você tiver gostos parecidos, também pode gostar dos artigos em https://trout.me.uk/lisp/
Sinto certa impaciência com a verificação formal de programas. Provar que um programa implementa corretamente uma especificação é teoricamente interessante, mas tem pouca utilidade prática
Escrever uma especificação correta é tão difícil quanto programar corretamente, então o problema difícil não é resolvido, apenas transferido. Há usos práticos para métodos formais, mas é raro encontrá-los
Uma vez que se consegue fazer isso, é possível impor como pré-condição. Por exemplo, exigir que se mostre que um array já está ordenado antes de passá-lo para determinada função
Foi escrito em 15 de maio de 2024, dia em que o Rust 1.0 completava 9 anos
Li o texto linkado do Boats e achei excelente. Fiquei surpreso que a citação de Hoare de 50 anos atrás ainda seja relevante, e que também seja tão bem formulada
Eu gostaria que fosse possível usar algo mais simples, como type guards em tempo de compilação. Quando os trait bounds proliferam, programas em nível de tipos ficam difíceis de ler
Por exemplo, coisas como
Where <<::Output as G>::Output as H>::Output: HList + Zoutype Output = <<::Output as G>::Output as H>::Output;. Aí você colocaCons>>>nisso e percebe que números como oU8do TypeNum também são, internamente, um aninhamento deCons>>. Dá para avançar nessa área e fazer as verificações desejadas, mas as mensagens de erro podem se afastar bastante da forma como desenvolvedores humanos escrevem código, e a implementação também é muito dolorosaA experiência do desenvolvedor é surpreendente porque isso não é “apenas uma função”, e sim uma combinação de genéricos específicos com tipos associados. Eu queria usar verificações em estilo runtime, mas executadas em tempo de compilação; para isso, porém, precisei escrever um código bem diferente. No fim, tornar o Rust em tempo de compilação em nível de tipos mais simples, funcional e legível talvez seja o caminho para que projetos desse tipo de análise formal ofereçam uma boa experiência a mantenedores e usuários. Em resumo, quero
comptimeem Rust. E também me pergunto seFuturebaseado emPin<&mut Self>já está cristalizado. Gostaria de experimentar outras implementações internas deasync/await, mas não sei por onde começar