Виталик предсказывает безошибочное будущее для смарт-контрактов

Источник: CryptoNewsNet Оригинальный заголовок: Виталик предсказывает безошибочное будущее для смарт-контрактов Оригинальная ссылка:

Обзор

Разработчики, ориентированные на безопасность, могут рассчитывать на то, что безошибочное программирование станет возможным в 2030-х годах, согласно мнению соучредителя Ethereum Виталика Бутерина.

После спорного форка Gnosis Chain для восстановления $9.4 миллиона, украденных в результате взлома Balancer, соучредитель Ethereum Виталик Бутерин заявил, что вера в то, что «ошибки неизбежны, невозможно создать безошибочный код», перестанет быть истиной в 2030-х годах.

Что сказал Виталик Бутерин о программировании?

Виталик Бутерин сделал прогноз, что безошибочный код станет реальностью в 2030-х годах, через взаимодействие в социальной сети X.

Обсуждение началось, когда Gnosis Chain объявила о выполнении жесткого форка 22 декабря. Этот форк восстановил $9.4 миллиона, украденных во время взлома Balancer в ноябре 2024 года, который истощил более $128 миллионов на нескольких блокчейнах. Восстановление потребовало, чтобы большинство валидаторов приняли новое программное обеспечение, а те, кто не обновился, столкнулись с штрафами.

Это вызвало некоторое сопротивление со стороны сторонников блокчейна, которые критиковали этот шаг, поскольку он противоречит принципу неизменности. Пользователь X с ником ‘colluding node’ заявил, что настоящая проблема заключается в том, как создаются блокчейн-приложения. Он утверждал, что использование смарт-контрактов в программируемых виртуальных машинах — неправильный подход.

«Есть всего 7 контрактов, которые стоит писать, и их следует закрепить в базовом слое и обеспечить безопасность за счет диверсификации клиентов», — написал пользователь.

Бутерин затем ответил, уточнив, что формально проверенный код не равен доказуемо безошибочному. Он даже предположил, что доказуемо безошибочный код может быть невозможен.

«Я бы даже сказал, что ‘доказуемо безошибочный’ — это невозможно, потому что ‘без ошибок’ означает ‘отсутствие разрыва между намерением и выполнением кода’, а наше намерение — чрезвычайно сложный объект, к которому у нас есть ограниченный доступ.»

Формальная проверка использует математические методы для проверки правильности работы систем, критичных к безопасности. Эта техника применяется с 1960-х годов в таких областях, как аэрокосмическая инженерия.

При использовании в смарт-контрактах формальная проверка может доказать, что бизнес-логика контракта соответствует заданной спецификации; однако, несмотря на то, что контракты Balancer были проверены 11 раз, проведенными четырьмя разными командами по безопасности, критическая ошибка все же прошла мимо.

Возможно ли будущее без ошибок в коде?

Бутерин предложил, что решение — в многоуровневой избыточности для устранения разрывов между намерением и выполнением. Он указал типовые системы как один из видов избыточности, а также формальную проверку конкретных утверждений о коде — как другой уровень.

Формальная проверка может обнаружить такие проблемы, как целочисленные переполнения и недополнения, повторный вход, плохая оптимизация газа, которые могут пройти мимо аудиторов и тестировщиков. В то же время, традиционное тестирование может лишь выявить наличие ошибок, а не их отсутствие.

Бутерин отметил, что некоторые программы продолжат иметь ошибки, потому что важнее функциональность, чем совершенство в некоторых случаях. Но разработчики, ориентированные на безопасность, будут иметь инструменты для достижения по-настоящему безошибочного кода.