Por que as pessoas não usam métodos formais? (2019)
Métodos formais para provar a correção de software continuam raros no desenvolvimento cotidiano, em grande parte porque são difíceis de aprender, caros de aplicar e muitas vezes vistos como desnecessários para aplicações de baixo risco, como apps CRUD ou plataformas sociais. Os კომენტadores destacam que técnicas rigorosas são adotadas principalmente onde falhas são extremamente custosas (por exemplo, projeto de hardware, bancos de dados, finanças, sistemas críticos), e que formas leves como sistemas de tipos, linters e verificação parcial são o compromisso mais prático. Vários argumentam que ferramentas de IA e melhor tooling poderiam reduzir a barreira de entrada, mas enfatizam que provas formais ainda deslocam o problema para escrever especificações precisas, que podem ser tão complexas e propensas a erro quanto o próprio código.
Valor Percebido e Contexto de Negócio
- Muitos argumentam que métodos formais raramente justificam seu custo: a maior parte do software é CRUD de baixo risco, protótipos ou aplicações de negócios em constante mudança, em que iterar rapidamente vence provas rigorosas.
- O maior ROI é visto em infraestrutura e domínios críticos para a segurança (bancos de dados, sistemas de arquivos, hardware, finanças, criptografia, aviônica, medicina, DeFi), mas mesmo aí a adoção é desigual.
- Alguns veem o subuso como sintoma de má gestão de risco e da cultura de “mover rápido”; outros enquadram isso de forma mais simples como otimização racional de ROI.
Dificuldade, Educação e Cultura
- Um tema recorrente: métodos formais são difíceis de aprender, intelectualmente exigentes e mal explicados; muitos engenheiros se intimidam ou não se interessam.
- Há confusão sobre qual método usar; as pessoas querem um “segundo melhor para tudo” em vez de um zoológico de técnicas.
- Defensores de métodos formais relatam resistência dentro das empresas e muitas vezes os “infiltram” em seu fluxo de trabalho.
Especificações vs. Código e Limites
- Vários comentários ressaltam que especificações podem ser tão complexas quanto código; os bugs podem simplesmente migrar da implementação para a especificação.
- A ordenação é usada para ilustrar como uma especificação “completa” é sutil (precisa capturar ordenação, comprimento, permutação, duplicatas, empates).
- Métodos formais são vistos como complemento aos testes, não como substituto; ambos acabam dependendo da compreensão humana dos requisitos.
Tipos, Verificação Parcial e Técnicas Pragmáticas
- Muitos observam que sistemas de tipos, linters e análises relacionadas já são amplamente usados como “métodos formais leves”.
- Há debate sobre onde termina a “verificação de tipos” e onde começa a “verificação formal”, com alguns insistindo que restrições no estilo de refinement como mínimo.
- A verificação parcial (por exemplo, provar propriedades-chave ou pequenos componentes puros) é apresentada como prática, especialmente para bibliotecas, codecs e algoritmos de concorrência.
Ferramentas, Exemplos e Estudos de Caso
- As ferramentas são vistas como fragmentadas e difíceis de abordar; as pessoas pedem soluções open source, amigáveis para iniciantes, de referência e exemplos não triviais (por exemplo, editor de texto, app de tarefas).
- Relata-se que hardware e algumas grandes empresas de software usam ferramentas formais mais pesadas; um praticante reescrevendo um motor de banco de dados em Rust usou model checking para provar a equivalência de mais de 1000 funções e descobriu bugs sutis a montante.
- Supostamente, alguns grandes provedores de nuvem usam modelos formais para design e validação de telemetria, mas os detalhes e a extensão disso são contestados.
LLMs e Direções Futuras
- Vários especulam que os LLMs poderiam mudar a equação ao:
- Gerar em massa provas ou especificações candidatas, que são mais baratas de verificar do que de produzir.
- Tornar viável que não especialistas experimentem ferramentas como TLA+, Lean e outras.
- Outros alertam que alimentar especificações formalmente precisas em um modelo caixa-preta reintroduz outra camada que, por si só, precisa ser confiável ou verificada.