При этом "аксиоматическая семантика", к которой я призываю в видео сильно проще в освоении, чем "денотационная семантика", которая требует по сути подробного описания всех денотаций и даже для простых примеров требует много времени и сил.
С позиции аксиоматического подхода вы можете сам решить на чем сфокусироваться и что проверить, не пытаясь делать полную верификацию всего кода. Но главное тут даже не то, что вы проверяете код, а то что формируете совсем иные паттерны анализа задачи. Это не работа над кодом, а работа над собой. По сути "зарядка для мозгов", которая нужна каждому, кто хочет повышать качество своего кода.