Как истинный шифропанк он установил локальную модель
gpt-oss:20b, и в твите пофлексил тем, что за час переписал свою платформу для ведения блога. При этом, офк, он понимает, что нормальная модель справилась бы с этим за one shot. Но тред не про вайбкодинг. Виталик написал тред про то, как AI должен использоваться в разработке Ethereum. И его позиция неочевидная.
the right way to use it, is to take half the gains from AI in speed, and half the gains in security: generate more test-cases, formally verify everything, make more multi-implementations of things
Необходимо направлять усилия не столько в скорость, как минимум половину — в безопасность. Больше тест-кейсов, формальная верификация всего, несколько независимых имплементаций одного и того же.
Формальная верификация — это когда корректность программы доказывается как теорема. Не "прогнали тесты, coverage 95%", а математическое доказательство, что при любых входных данных контракт ведёт себя правильно. До сих пор это стоило столько, что делали только там, где баг приводит к ужасным проблемам. На вскидку даже не нашел смарт-контракты с реализованной формальной верификацией сейчас из дефи топа. Верифицировать 20-строчный контракт стоило дороже, чем написать.
Один из контрибьюторов Lean Ethereum с помощью AI написал machine-verifiable proof для одной из самых сложных теорем, на которых стоит безопасность STARKs. Из людей, кто реально понимает всю эту цепочку до конца — может пара сотен в мире. И вот для этой математики теперь пишутся формальные доказательства с помощью AI.
bug-free code, long considered an idealistic delusion, will finally become first possible and then a basic expectation
Bug-free code — который всю жизнь считался бредом идеалистов — скоро станет сначала возможным, а потом базовым ожиданием. Виталик прямо это говорит. Для блокчейна, где весь смысл в том что ты не доверяешь никому, это необходимая часть пазла.
При этом без розовых очков — "there WILL be lots of wrestling with bugs and inconsistencies between implementations". Но эта борьба будет идти в 5x быстрее и 10x тщательнее.
В исходной цитате треда — чел, который за две недели один написал Ethereum-клиент на весь роадмап 2030+. 702K строк Go, синхронизируется с мейннетом. Виталик признаёт — там полно стабов и багов. Но полгода назад даже это было невозможно.
Но глядя на Виталика мне кажется, что до сингулярности ещё далеко.
https://x.com/VitalikButerin/status/2027781104288317837