История изменений

Но кто мне помешает взять твой World (или память) и раскидать его копии по десятку разных функций?

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

Вот у тебя есть чисто функциональная спецификация IO которая в качестве модели состояния использует чисто функциональную же структуру данных (какой-то тип, словарь, функция из адресов в значения как модель «массива») для моделирования состояния, она работает ожидаемым образом. Дальше можно доказывать какие-то теоремы — как сочетаются чтение и запись, например. Если теперь хочется чтобы всё это работало с настоящим внешним состоянием, то эту структуру данных нужно заменить на фиктивную абстрактную которая будет вести себя как внешнее состояние, так, как должна. Если «реальный мир» будет себя вести как полагается, то все теоремы из спецификации останутся в силе, если «реальный мир» не ведёт себя как «реальный мир» — извините. Это как с примитивными операциями — они вводятся в язык одними сигнатурами, не определениями, реализуются подходящим для данной архитектуры способом, либо внешними библиотеками, то что железо или RTS библиотеки работают как должны и то что свойства этих операций такие, какими они должны быть можно только постулировать (в агде для этого есть ключевое слово postulate, фактически — axiom).

Но кто мне помешает взять твой World (или память) и раскидать его копии по десятку разных функций?

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

Вот у тебя есть чисто функциональная спецификация IO которая в качестве модели состояния использует чисто функциональную же структуру данных (какой-то тип, словарь, функция из чисел в значения как модель «массива») для моделирования состояния, она работает ожидаемым образом. Дальше можно доказывать какие-то теоремы — как сочетаются чтение и запись, например. Если теперь хочется чтобы всё это работало с настоящим внешним состоянием, то эту структуру данных нужно заменить на фиктивную абстрактную которая будет вести себя как внешнее состояние, так, как должна. Если «реальный мир» будет себя вести как полагается, то все теоремы из спецификации останутся в силе, если «реальный мир» не ведёт себя как «реальный мир» — извините. Это как с примитивными операциями — они вводятся в язык одними сигнатурами, не определениями, реализуются подходящим для данной архитектуры способом, либо внешними библиотеками, то что железо или RTS библиотеки работают как должны и то что свойства этих операций такие, какими они должны быть можно только постулировать (в агде для этого есть ключевое слово postulate, фактически — axiom).