Время и технологии подошли к тому чтобы разрабатывать настоящий экскаватор, а не лопату по лекалам 60-х, но "с новой удобной ручкой". И, что бесит, судя по научным работам — "они там" это отлично понимают. Научных работ по интеграции Coq, Dafny, TLA+ и других с LLM дофига.
А у нас — чёт я сомневаюсь что это направление даже обсуждается кем-то. По крайней мере ни на хабре, ни на rsdn — не видно и не слышно. А учитывая что GPT и её аналоги скорее всего будут доступны только по подписке, и для нас доступ будет закрыт — серьёзен риск что в век экскаваторов мы придём с плохо задокументированной суверенной лопатой