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

нет у меня никакого заблуждения. Рынок диктуют ничего не смыслящие юзеры которым надо лиж бы чтоб кнопочки были покрасивее  ( а что тормозит - то нормально) и планктон программеров корпораций, которые по большей части пьют кофе и болтают на работе, а пишут по 20 строк кода в день. Я не исхожу завистью, мне просто обидно. Вроде в других отраслях типа машиностроения, такого же вроде бы нету, там за каждый грамм материала борются.
Что мешает применить принципы модель чекинга в новой Винде, заместа новых дурацких кнопок, и построить нормальный механизм коррекции ошибок ( а не убожество, например в 7-й, которое несколько минут будет че то пережевывать а потом выдает неизвесная ошибка).
Так ну это отклонение от темы.
Дополнение.
- Полученный по методу описанному выше автомат может (должен) быть минимизирован  Например поиск выражений "всегда правда" или "всегда ложь", сокращение по взаимосвязи переменных а потом просто компилируется в автоматон - почти как по теории. Че то тут можно пообсуждать
- А еще немаловажный момент ( который правда на лекциях не рассматривался, но из имеющихся знаний можно вывести) - это контроль состояния при нескольких паралельных процессах. Очевидно, что тогда имеем недетерминисткий аутоматон (НФА), находящийся сразу в нескольких состояниях, не меньших чем количество процессов. НФА вообще компактнее (аналогичный ДФА имел бы 2^n  состояний где n- все состояния НФА. Только реализовывать его несколько сложнее, эффективнее статическим массивом состояний.
А в игрушке NuSMV нет даже оптимизации, например условие x = {0..400} приводит к появлению четырехсот новых состояний автомата, заместо одного с переходом по условию (0 <= x)  И ( x <=400).