Não Confie na Intuição, Prove: O Futuro da Codificação Baseada em Provas

A codificação baseada em provas não é uma novidade teórica, já está em uso real em sistemas críticos, como o kernel do sistema operacional CertiKOS (verificado em Coq) e o compilador CompCert (também em Coq), ambos comprovadamente livres de bugs de execução. O que muda agora é a tentativa de levar essa rigorosidade para fora dos laboratórios acadêmicos e de segurança crítica: o 'vibe coding' citado na notícia é um nome informal para técnicas que usam tipos dependentes para transformar especificações em exigências de compilação, ou seja, o código só compila se provar matematicamente que faz o que promete. Linguagens como Idris 2 e Lean 4 já permitem isso com relativa praticidade; o F* da Microsoft, por sua vez, é usado industrialmente em projetos de criptografia e contratos inteligentes.

O foco atual não é mais só provar que um algoritmo está certo, mas integrar a prova ao fluxo de trabalho diário, daí ferramentas como Verus (2024, DARPA/CMU) para Rust e Spoq (2023, Columbia) para C. Ambas reduzem drasticamente o esforço manual de escrita de provas, automatizando passos repetitivos sem sacrificar garantias formais. Isso é crucial: a barreira histórica nunca foi a matemática, mas a produtividade do engenheiro.

Software com falhas de lógica ou segurança custa bilhões por ano, só em 2025, incidentes ligados a erros de memória em C/C++ geraram mais de US$ 2,1 bilhões em perdas diretas, segundo relatório da Synopsys. A verificação formal não elimina testes, mas antecipa falhas que testes unitários ou de integração raramente pegam: condições de corrida em concorrência, overflow silencioso, comportamento indefinido. Em setores como automotivo (ISO 26262), aeroespacial (DO-178C) e finanças descentralizadas (smart contracts), essa garantia não é luxo, é requisito legal. E, com a IA assumindo tarefas de geração de código, a necessidade de provas formais só aumenta: você pode confiar no modelo, mas não pode confiar em tudo o que ele escreve.