Как математически описывают «потоки»?

новомодные потоки

Им правда уже 100500 лет.

«Потоки» – это просто FIFO.

(Стек для ставнетия – LIFO)

о многопоточном коде можно рассуждать методом Овицки-Гриза (искать owicki-gries)

https://mediatum.ub.tum.de/doc/601717/601717.pdf

если к практике переходить, сейчас так же модно всё это как то сочетать например с тем что называется permission-based reasoning http://viper.ethz.ch/tutorial/#permissions

(хотя и в первом документе вполне себе практика)

прям если описать, то можно с помощью монады недетерминированного выбора например.

https://wiki.haskell.org/Nondeterminism,_monadically

ну конечно надо упомянуть конкурентрую логику с разделением
https://read.seas.harvard.edu/~kohler/class/cs260r-17/brookes16concurrent.pdf

короче тут вступление будет на академический час наверное..

потоки надо вычитывать последовательно

man 3 fseek

Как…

Индукции и рекурсии «хватит всем» :)

Вот прям совсем поток чисто математически описывается так же, как цифровая обработка аналоговых сигналов. Куча литературы на эту тему есть, в общем-то. Фильтры там, задержки и пр. Всякий парсинг вполне можно описать как цифровой фильтр, например. Правда такой подход на практике не очень эффективен, но если интересует чисто теоретические измышления - то пуркуа бы и не па.

https://proofassistants.stackexchange.com/questions/74/proof-assistants-with-support-for-creating-executable-software-artifacts

Раньше были «ленты» (в 1936-м году, у Тьюринга и у Поста). Ленты можно было читать в любом направлении, перемещаться и туда, и обратно, и куда-попало. А потоки не такие, потоки надо вычитывать последовательно и они могут заканчиваться (а ленты по определению были бесконечные).

Так вот, как математики эти новомодные потоки описывают, когда доказывают корректность программ?

Если ты видел доказательства теорем про машины Тюринга, то чем они по-твоему должны отличаться от аналогичных доказательств про fifo/lifo ? Такое впечатление, что ты просто мало знаком с предметом..

Поток это просто функция read :: (world_in) -> (world_out, datum). Ну или write :: (world_in, datum) -> (world_out) для записи. Где world_in и world_out это некоторые значения с неизвестной структурой, а datum это элемент потока (бит, байт, символ и тд и специальные значения для конца потока, ошибки и тд, если тебе это надо).