Вот 5 ключевых идей из выступления @thejonanshow на ETHDenver 2025.

1. Важность формальной верификации
Джоан подчеркивает, что формальная верификация предоставляет математические доказательства поведения программ, что может быть критично для сложных систем. Он отметил, что хотя это не гарантирует полную правильность программы, она позволяет разработчикам заявить о определенных инвариантах внутри своих систем. Например, заявление о том, что общий баланс банка никогда не должен падать ниже нуля, показывает, как специфические правила можно проверить для поддержания целостности системы.

2. Инициатива открытого исходного кода от Certora
Джоан поделил радостные новости о компании, в которой он работает, Certora, которая недавно сделала открытым исходный код своего проверяющего инструмента для формальной верификации. Эта инициатива нацеливается на упрощение процесса формальной верификации, делая инструмент более доступным для разработчиков программного обеспечения. Он поощрил участников попробовать его, подчеркивая его простоту использования и потенциальные преимущества для повышения надежности программ.

3. Недопонимания о формальной верификации
По словам Джоана, многие люди вне пространства Web3 имеют недопонимания о формальной верификации, часто считая ее непрактичной на основе устаревших представлений. Он подчеркивал, что современные приложения могут значительно выигрывать от формальных методов, указывая на то, что хотя доказательство каждого аспекта сложной системы может быть не всегда возможным, важные инварианты можно и нужно проверять, чтобы избежать серьезных проблем.

4. Смещение к декларативному программированию
Джоан выступал за переход от императивного к декларативному программированию, подчеркивая, что инженеры программного обеспечения часто программируют в деталях, а не определяют желаемые результаты. Этот переход может позволить программному обеспечению определять, как достичь указанных результатов, что может снизить сложность и упростить интеграцию с технологиями искусственного интеллекта, которые могут помочь в разработке программного обеспечения.

5. Влияние ИИ в разработке программного обеспечения
Джоан отметил растущее интегрирование ИИ в рабочие процессы разработки программного обеспечения. Хотя он признал эффективность, которую ИИ может принести, он выразил опасения по поводу тенденции ИИ "галюцинировать" или производить неожиданные результаты. Он аргументировал необходимость надежных методов формальной верификации для выявления расхождений, которые могут возникнуть при использовании ИИ, утверждая, что четкие инварианты могут защитить от таких проблем.

Вы можете посмотреть наши полные идеи здесь, 100% бесплатно: https://t.co/bQ2B2KBeCc