>> математически доказанное отсутствие ошибок иногда нужно.
> Гражданин Тюринг (знаете такого?) в свое время сформулировал и доказал теорему, суть
> которой сводится к следующему: некая программа не может выдать определенный вердикт
> относительно другой произвольно взятой программы. Он брал в качестве примера анализ
> того факта завершится ли программа за конечное время или нет, однако
> как следствие, это распостраняется и на анализ иных вариантов поведения программ.
> Вы хотите сказать что Тюринг был дурак, его доказательство ничтожно и один
> вы тут такой умный, что можете предложить "математически доказанное отсутствие ошибок"?
> А как это математическое доказательство строится, если Тюринг доказал ровно обратное?

Тьюринг был умный, но его результаты надо тоже использовать с умом, а не размахивать ими как фаллической дубиной народного гнева. Результат Тьюринга, если Вы заметите (для этого надо прочитать, surprise, собственные слова), говорит про анализ *произвольно* взятой другой программы. В случае же доказательной верификации программы эта программа ничуть не "произвольна", она хорошо известна - более того, она специально пишется так, чтобы её можно было верифицировать используемыми средствами. Это отдельное достаточно сложное искусство - такое написание.

И подумайте вслед, что "любая программа" и "любая цель программы" - несколько разные вещи. Второе в принципе достижимо, даже если неподъёмной ценой. Первое - нет, что и доказал Тьюринг.