Глупости написаны. Период жёсткого формализма закончен. Современные программы слишком сложны, чтобы можно было провести формальное доказательство корректности. Да что там программирования, похожая ситуация в математике. Современные численные методы эмпирические. Их сходимость не доказана. В них нарушаются математические правила. Чтобы не быть голословным — в градиентных методах (CG, SCG, BiCG, BiCGStab) используется эренгетическая норма по некоторой матрице, которая, по определению, должна быть симметричной и положительно определённой. Для того, чтобы применить его к произвольной матрице, строят специальную, вдвое большей размерности, коорая заведомо симетрична. Но не положительно определена. Метод, чья правильность (сходимость и аппроксимация) доказана для положительно определённых матриц абсолютно незаконно применяется для произвольных матриц. И на этом алгоритме работают модели АЭС, самолётов, космических кораблей. Вроде работает...