есть что-то почитать по поводу вывода типов? не представляю вообще как такое проворачивать.

есть что-то почитать по поводу вывода типов? не представляю вообще как такое проворачивать.

У Душкина есть перевод статьи про вывод по Хиндли-Милнеру. Если коротко, то выписываем систему уравнений и решаем её.

Программисту имеющему опыт за рамками паскального семейства средств разработки (ну Дельфи, короче)  практически нечем соблазниться. Не ищите там рационального зерна, это религия. Или как хобби (у меня, например :) Основные "жертвы" оберона - это школьники или люди из других профессий (не профессионалы в программировании), которые наслушались про "16 страниц, супер язык". Есть, как всегда, единичные исключения осмысленного применения на практике, но надо искать...

В целом для таких задач хватает просто DSL со строгой типизацией и строгими правилами для программиста в духе запрета на неинициализированные переменные. А от переполнения стека я вообще радикальным образом избавился — стека нет. Ну, рекурсии тоже нет — но кто ее в своем уме на МК использует? %)

В обобщениях ничего плохого нет. Поиски разных вариантов перворода в свое время привели к побочным полезным результатам. Главное -- не ударяться в догматизм.

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

Далее, для реализации какого-нибудь RISC-V можно ввести init (начальное состояние) и next (переход из состояния в состояние). Для практической реализации остается только рассказать про хвостовую рекурсию и CPS.

С чего это? Объекты - это замыкания. Вы можете, конечно, описаывать объекты, рисуя картинки, и размахивая руками, но когда потребуется дать строгую семантику, вам придётся описывать это всё функциями. Других способов люди пока не придумали. Да и не факт, что другие способы вообще существуют.

пи-исчисление тоже к функциям сводится?

Ну... Для новичка это может быть и самый верный подход. Но всё же имеет смысл продвинуться дальше. В ТК есть полезные вещи, которые позволяют просто доказывать нетривиальные результаты. Параметричность, например

Ну, это отвлеченно. Настолько отвлеченно, что, кажется, далеко от нужд обычных системных программистов и компиляторщиков.

А если говорить конкретнее? Я, например, легко себе представляю, что можно интересного показать и доказать, используя моноид переходов.

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

Ну ув. Михаил, вся математика - это набор языков для описания реальности. Причём эти языки могут быть совершенно эквивалетны. Например, классическая механика может быть описана как законами Ньютона, так и принципом наименьшего действия. И перейти можно как в одну сторону, так и в другую. Более того, нет никакой возможности понять "а что же на самом деле".

Так и тут с монадами.