В этом смысле - да, практически оно самое.
Но тут два "но": во-первых, я её не осилил, даже описание самой содержательной логики до конца не дочитал, во-вторых, Зиновьев ввёл содержательную логику в противовес полностью формальной математической для рассуждений о физике. Так что оно как бы не 100% формальное. Но с точки зрения "нормальных людей" эта "содержательная логика" очень формальная. 😃

про системы типов в том варианте, который подразумевался в исходном чате - через лямбду, обычно рекомендуют Пирса. но она для computer scientists. есть еще классик Барендрегт, он ужаснее)). вообще книг сотни, но большинство для программеров. либо совсем передовые статьи. http://ropas.snu.ac.kr/~kwang/520/pierce_book.pdf

а про теорию категорий light version это Спивак, наверное https://arxiv.org/pdf/1302.6946.pdf

Христофор, надо как раз книгу про типы для непрограммеров. Как BORO для не онтологов.

А такие бывают?

См. название чата. Там не только про программирование.

@unmuamua Если в принципе нет, то типы нужны только для внутренней программистской кухни, и ничего на них не построить про предметный домен.

Так может просто никто не пробовал? На днях проскакивала ссылка на моделирование для F#, где она?

DDD+F#, но там тоже "вот у нас есть алгебраические типы, это лучше, чем объекты"

Более лайт это Милевский?)

На всякий случай к коллекции нематематических логик - Non-Axiomatic Logic (NAL) и Non-Axiomatic Reasoning System (NARS) by Pei Wang: https://cis.temple.edu/~pwang/

Правда, я сомневаюсь, что она применима для моделирования чего-либо кроме AGI...

Я смотрю на это так, что программер (и пруф-инженер) пишет программу по заданной спецификации, ТЗ, используя свои типы. Спецификацию готовит, в лучшем случае, инженер по требованиям. Инженер этот использует описание мира, подготовленное онтологическими инженерами.  Получается, что напрямую программер с онтологами не стыкуется нигде. Вместо это некий инженер по требованиям должен перевести с языка, понятного онтологам, на язык, понятный программеру.

Милевский не то, чтобы лайт, но он жестко для программеров.

И, кстати, да, может АТД действительно лучше чем объекты?

ну если онтологи запишут свою "онтологику" сразу конструктивно, то может и не нужен переводчик :)

на данный момент нужен же ))

Повторю ссылку: https://pragprog.com/book/swdddf/domain-modeling-made-functional

а вторая книга про реактивное вам не пошла кстати?

напоминаю кстати что я эти книги нашел за 1 минуту гугления

поэтому не стоит их рассматривать как некую вершину