Os desenvolvedores que priorizam a segurança podem esperar que a codificação sem bugs se torne alcançável na década de 2030, de acordo com o cofundador da Ethereum, Vitalik Buterin.
Após o controverso hard fork da Gnosis Chain para recuperar $9,4 milhões do hack da Balancer, o cofundador da Ethereum, Vitalik Buterin, disse que a crença de que "bugs são inevitáveis, não se pode fazer código sem bugs" deixará de ser verdade na década de 2030.
O que disse Vitalik Buterin sobre codificação?
Vitalik Buterin fez uma previsão de que o código sem bugs se tornará uma realidade na década de 2030 através de uma interação na plataforma de redes sociais, X.
A discussão começou quando a Gnosis Chain anunciou que executou um hard fork no dia 22 de dezembro, conforme reportado pela Cryptopolitan. O hard fork recuperou $9,4 milhões roubados durante a exploração da Balancer em novembro de 2024, que drenou mais de $128 milhões através de múltiplas blockchains. A recuperação exigiu que a maioria dos validadores adotasse um novo software, e aqueles que falharam em atualizar estão a enfrentar penalidades.
Isto, claro, foi recebido com alguma resistência por parte dos apoiantes da blockchain que criticaram a medida porque vai contra o princípio da imutabilidade. Um utilizador do X com a alcunha 'colluding node' disse que o verdadeiro problema é como as aplicações blockchain são construídas. Eles argumentaram que usar contratos inteligentes em máquinas virtuais programáveis é a abordagem errada.
"Existem apenas 7 contratos que valem a pena escrever, e eles deveriam simplesmente estar consagrados na camada base e obter segurança da diversidade de clientes," escreveu o utilizador.
Buterin então respondeu esclarecendo que formalmente verificado não equivale a comprovadamente sem bugs. Ele foi mais longe ao sugerir que código comprovadamente sem bugs pode nem sequer ser possível.
"Eu iria até ao ponto de dizer que 'comprovadamente sem bugs' não é possível, porque 'sem bugs' significa 'nenhuma lacuna entre intenção e execução do código', e a 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 áreas como a engenharia aeroespacial.
Quando usada em contratos inteligentes, a verificação formal pode provar que a lógica de negócio de um contrato atende a uma especificação predefinida; no entanto, apesar do facto de os contratos da Balancer terem sido auditados 11 vezes, realizadas por quatro empresas de segurança separadas, uma falha crítica ainda passou despercebida.
É possível um futuro de código sem bugs?
Buterin propôs que a solução são múltiplas camadas de redundância para filtrar lacunas entre intenção e execução. Ele apontou os sistemas de tipo 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 detetar problemas como underflows e overflow de inteiros, re-entrância e otimizações de gas inadequadas que podem passar despercebidos aos auditores e testadores. Entretanto, os testes tradicionais só podem verificar a presença de erros em vez da sua ausência.
Buterin observou que alguns softwares continuarão a ter bugs porque os ganhos de funcionalidade são mais importantes 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.
Aperfeiçoe a sua estratégia com mentoria + ideias diárias – 30 dias de acesso gratuito ao nosso programa de negociação
Fonte: https://www.cryptopolitan.com/vitalik-predicts-bug-free-smart-contracts/
