> для идеальности нужна мат модель и анализатор логики.О какой матмодели ты сейчас говоришь? О матмодели программы? То есть о спецификации программы, написанной на формальном языке? Это может помочь, но во-первых, есть ограничения такого подхода, во-вторых это переход с C/C++ на язык описания спецификаций.
Программист-человек может качественнее проводить аудит кода потому, что он может по коду угадать намерения того, кто писал код. Но, самое что забавное, угадать эти намерения возможно только одним путём: взять модель психики программиста и дальше разглядывать код и статистическим путём пытаться угадать состояние психики, которое с максимальной вероятностью породит именно такой код.
То есть, тут нужна формальная модель психики программиста. И этим и обусловлен вопрос выше: может ты об этой модели?
Человеку удаётся справиться с этим, потому что он сам себе модель программиста, писавшего код. А статистику всю нейросетки в его голове считают.
ИИ сейчас подошёл вплотную к тому, чтобы реализовать нужную статистику. А это автоматически означает, что какая-никакая модель программиста у ИИ уже есть. Остался один шаг -- сделать эту модель каузальной, а не корреляционной. Но это, я полагаю, произойдёт после того, как хайп на deep-learning спадёт: все самым натуральным образом сначала тянутся за низковисящими фруктами и лишь когда они кончатся, начинают чесать репу: как достать остальные?
Но я к тому, что с этой перспективы, статистический поиск багов -- это шаг в нужном направлении. Либо мы движемся в направлении выдачи компилятору всё большего количества информации о задумке программиста (а это всякие расты, или даже формальные языки спецификаций программ), либо мы учим ИИ угадывать эту задумку по тому, что есть. И вот это второе, естественно напрашивается делать так, как это делает человек, то есть статистически.
