ИИ-агенты становятся очень хороши в написании кода — и очень хороши в том, чтобы его ломать.
В эпоху агентов для критически важного ПО фразы «тесты прошли» будет уже недостаточно. Нам нужно уметь доказывать свойства кода, который мы выпускаем.
И это уже становится практичным.
У Rust уже есть Aeneas → Lean. Microsoft Research использует его для формальной верификации SymCrypt. У Java и C тоже уже есть основа в формальной верификации.
C# не должен остаться позади.
ИИ может написать код.
ИИ может построить доказательство.
А детерминированное ядро проверки доказательств проверит, действительно ли это доказательство корректно.
Это совсем другая модель доверия по сравнению с
ИИ пишет код → ИИ проверяет код → надеемся, что оба оказались правы.
Предложение: https://github.com/dotnet/csharplang/discussions/10314
@KodBlog
