O Caso Contra a Verificação Formal, 50 Anos Depois

Artigo original ↗ Discussão no Hacker News ↗

A verificação formal de software é revisitadda à luz de uma famosa crítica de 1979, com muitos argumentando que, embora provas completas de ponta a ponta ainda sejam impraticáveis para sistemas reais e desorganizados, a verificação direcionada de componentes críticos (por exemplo, datastores distribuídos, compiladores, mecanismos de políticas) é tanto viável quanto valiosa. Os comentários destacam que especificar comportamento rigorosamente costuma ser mais difícil do que escrever código, que a lacuna entre modelo e código e a evolução dos requisitos limitam o alcance das provas, e que a maioria das falhas reais decorre de especificações defeituosas ou inconsistentes, e não de bugs de implementação. Há um otimismo cauteloso de que sistemas de tipos mais poderosos, ferramentas melhores e assistência por IA possam tornar os métodos formais mais acessíveis, mas também preocupação de que provas cristalizem maus projetos e de que os incentivos econômicos ainda favoreçam software “bom o suficiente” em vez de correção matematicamente garantida.

Escopo e praticidade da verificação formal

  • Muitos veem a verificação de sistemas completos como intratável para produtos bagunçados e em evolução (por exemplo, redes sociais, GUIs), mas concordam que verificar subsistemas e propriedades específicas é valioso.
  • GUIs são vistas como especialmente difíceis de especificar; alguns mencionam abordagens de GUI baseadas em restrições como mais próximas de especificações, principalmente para evitar bugs óbvios de interface.
  • Vários comentários enfatizam que não há necessidade de “tudo ou nada”: verificar permissões, idempotência de APIs, consistência distribuída e propriedades de ausência de perda de dados já é extremamente útil.

Verificação formal vs testes

  • A verificação é apresentada como garantia de propriedades para todas as execuções, enquanto os testes amostram execuções.
  • Testes baseados em propriedades e testes de mutação são discutidos como técnicas intermediárias; fuzzing e testes aleatórios se beneficiam de especificações claras.
  • Alguns argumentam que deveríamos pensar em métodos formais como “testes com esteroides”, não como substitutos.

Especificações: benefícios, dificuldade e correção

  • Há discordância sobre se especificações são mais fáceis de entender do que código: alguns acham especificações formais mais concisas e próximas da intenção; outros as consideram mais difíceis do que implementações.
  • Exemplos históricos (operações de ponto flutuante, compressão, sistemas de arquivos, bancos de dados, redes) são citados como casos em que as especificações são simples e as implementações são complexas.
  • Um longo subthread sobre “ordenação” ilustra como especificações aparentemente triviais são fáceis de errar sutilmente, reforçando que escrever especificações corretas também é difícil.
  • Surge a հարցao: por que assumir que a especificação é mais correta do que o programa? Respostas: verificar muitas vezes é mais fácil do que construir; especificações podem ser mais simples; mas erros de especificação são reais e devem ser tratados como bugs.

Economia, incentivos e regulação

  • Economias no estilo de hardware (bugs custam milhões) justificam verificação pesada; software normalmente depende de correções baratas posteriormente.
  • Alguns argumentam que software robusto já existe onde os compradores pagam por isso (bancos, aviação); outros observam que o software de consumo típico continua com bugs.
  • Há preocupação de que “selos” regulatórios de verificação possam virar carimbos burocráticos sem ganhos reais de qualidade.

IA, ferramentas e a lacuna modelo–código

  • Limitações passadas incluíam notações ruins e poder de computação insuficiente; solucionadores modernos SAT/SMT, assistentes de provas e LLMs aliviam parte do peso.
  • A IA atualmente é mais eficaz nas mãos de especialistas; há esperança de que agentes eventualmente gerem especificações e provas para módulos profundos com invariantes simples.
  • A lacuna modelo–código (por exemplo, especificação em TLA+ vs código em Rust) é vista como um problema central; mitigations sugeridas incluem:
    • Assistentes de prova que geram código executável.
    • Linguagens e ecossistemas (por exemplo, SPARK/Ada, sistemas de tipos mais ricos, motores de políticas verificados) em que especificações e código sejam fortemente integrados.
  • Alguns temem que provas e testes de granularidade fina congelem abstrações ruins e dificultem refatorações.

Requisitos vs implementação

  • Vários participantes argumentam que, em muitos projetos reais, as principais falhas são requisitos inconsistentes ou impossíveis, não código incorreto.
  • Eles sugerem que a maior necessidade é de ferramentas que ajudem a formalizar e verificar requisitos contra restrições técnicas e de negócio, e não apenas implementações.