Я периодически пытаюсь прочесть "Дисциплину программирования" Дейкстры.

Я высказываю простую мысль: что все взаимодействующие активные сущности системы инкапсулируют в себе некоторое состояние. В совершенно простом и понятном смысле. Автоматном, например.

Сердечно одобряю.

Действительно, Дейкстра может быть и трудноват для начинающих.
Поробуйте Д.Гриса ("Наука программирования").
Там помягче, поподробней.
А примеры другие, так что пересечений не будет.

Миль пардон. Как раз уж с БД Вы никуда не денетесь от состояния. Один и тот же запрос Вам может вернуть разные данные.

Да ну. Знание основ исчисления предикатов и приобретённый с опытом навык анализа состояний процессов. Куда уж до лямбда-исчислений и теорий категорий.
Или Вы всё про то же - про то, что ФП лучше защищено "от дурака"? Не разломаешь? Можно посмотреть образцы и ваять, а язык будет бить по рукам? Ну, что ж Вы хотите: Дейкстра - это анализ. С большой буквы Анализ. Инструмент понимания задач, а не просто формальная система.

Что это даёт по сравнению с тем же equational reasoning в ФП?

А Вы часто применяете equational reasoning?

... Скажите, Вы сами реально используете эту дисциплину ... методично, от начала до конца?

Но суть зла в виде "глобальности" - остается.

Математики тоже не выписывают полностью свои доказательства, потому что это невозможно.

Суть не в том, чтобы все обоснования выписывать "методично, от начала до конца", а в том, чтобы написать доказательство (программу) так, чтобы в любом месте можно было в случае необходимости уточнить.

Математики опираются на ранее доказанные теоремы. В программировании такой опоры практически нет. На что программистам-то опираться?

А в чём, собственно, зло?

Хорошо. Скажите, Вы сами реально используете эту дисциплину? Не один раз на десяток программ, что бы побаловаться или решить серьёзную проблему в программе, а так, что бы методично, от начала до конца? Или Вы считаете, что конкретно Вы можете ограничиться редкими ассертами, а полностью все эти предикаты выписывать необязательно?

Отсутствие контроля - кто, где и когда имеет доступ к стэйту. В добавок к этому - неочевидные зависимости. В добавок к этому - проблемы в многопоточной среде. Короче, лучше один раз "разгрести", чем сто раз прочитать

Так ведь он для того и сделан глобальным, что бы доступ к нему имел кто угодно.

Он реализован потокобезопасным, так как доступ к нему имеет кто угодно.

Про неочевидные зависимости не понял.

Здесь проблем с "глобальностью" встречаться и не должно.