Vitalik prevê futuro sem bugs para contratos inteligentes

Desenvolvedores que priorizam a segurança podem esperar que a programação sem bugs se torne viável na década de 2030, de acordo com o co-fundador do Ethereum, Vitalik Buterin. 

Após a controversa bifurcação dura (hard fork) da Gnosis Chain para recuperar $9,4 milhões do hack do Balancer, o co-fundador do Ethereum, Vitalik Buterin, disse que a crença de que "bugs são inevitáveis, você não pode fazer código sem bugs" deixará de ser verdadeira na década de 2030.

O que Vitalik Buterin disse sobre programação? 

Vitalik Buterin fez uma previsão de que o código sem bugs se tornará uma realidade na década de 2030 por meio de uma interação na plataforma de mídia social, X. 

A discussão começou quando a Gnosis Chain anunciou que executou uma bifurcação dura em 22 de dezembro, como reportou pela Cryptopolitan. A bifurcação dura recuperou $9,4 milhões roubados durante a exploração do Balancer em novembro de 2024, que drenou mais de $128 milhões em várias blockchains. A recuperação exigiu que a maioria dos validadores adotasse um novo software, e aqueles que falharam em atualizar estão enfrentando penalidades.

Isso, claro, foi recebido com alguma resistência por apoiadores da blockchain que criticaram a movimento porque vai contra o princípio da imutabilidade. Um usuário do X com o apelido de 'colluding node' disse que o problema real é como as aplicações blockchain são construídas. Eles argumentaram que o uso de contratos inteligentes em máquinas virtuais programáveis é a abordagem errada. 

"Existem apenas 7 contratos que valem a pena escrever, e eles deveriam apenas ser consagrados na camada base e obter segurança da diversidade de clientes", escreveu o usuário. 

Buterin então respondeu esclarecendo que verificação formal não é igual a comprovadamente sem bugs. Ele foi além e sugeriu que o código comprovadamente sem bugs pode nem ser possível.

"Eu diria até que 'comprovadamente sem bugs' não é possível, porque 'sem bugs' significa 'sem lacuna entre a intenção e a execução do código', e nossa intenção é um objeto extremamente complexo ao qual temos apenas acesso limitado." 

A verificação formal usa métodos matemáticos para verificar se sistemas críticos de segurança funcionam corretamente. A técnica tem sido usada desde a década de 1960 em campos como a engenharia aeroespacial. 

Quando usada em contratos inteligentes, a verificação formal pode provar que a lógica de negócios de um contrato atende a uma especificação predefinida; no entanto, apesar do fato de que os contratos do Balancer foram auditados 11 vezes, conduzidos por quatro firmas de segurança separadas, uma falha crítica ainda passou despercebida. 

Um futuro de código sem bugs é possível? 

Buterin propôs que a solução é múltiplas camadas de redundância para filtrar lacunas entre a intenção e a execução. Ele apontou os sistemas de tipos como uma forma de redundância e a verificação formal de reivindicações específicas sobre o código como outra camada.

A verificação formal pode detectar problemas como underflows e overflows de inteiros, re-entrada e otimizações de gás inadequadas que podem passar despercebidas por auditores e testadores. Enquanto isso, os testes tradicionais só podem verificar a presença de erros, em vez de sua ausência.

Buterin observou que alguns softwares continuarão tendo bugs porque os ganhos de funcionalidade importam mais do que a perfeição em certos casos. Mas os desenvolvedores que priorizam a segurança terão as ferramentas para alcançar código verdadeiramente sem bugs.