Обсуждение

"в этот тредик кастуется sober-space".

Частные формализации будут всегда удобнее. Естественный Дао потечет так: разовьются богатые частные формализации, там и сям добьются своих успехов, потом через много лет их осенит что делают часто одно и тоже. И надо разговаривать на одном языке про то, что только спинным мозгом чувствуется как "одно и то же". И вот тогда опять, как было много раз уже, поможет ТК. Можно делать и сразу правильно, но для этого нужно обладать очень плохим характером и огромной верой в правильность выбранного пути. :))

Я чуток затронул этот вопрос в посте о микросервисах: http://ailev.livejournal.com/1155033.html "Микроформализации" (микротеории) против "теории всего" обычно начинают и выигрывают. Общий формализм нужен только для обсуждения того, что и как делать с микротеориями при обсуждении, затрагивающем самые разные формализмы.

А следовательно, правилен путь который предлагаю я: сделать софт для обучения рассуждениям в струнных диаграммах. Сделать ТК, представленный в простой ненавязчивой форме, элементом чьей-то (большой вопрос - чьей?) культуры.

Я б тут согласился с Баезом (чуть-чуть дополнив трассировками к модулям): принципиальные схемы в архитектурах и их трассировки к модулям могут быть такими диаграммами.

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

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

А скажите, как смоделировать виртуальную машину и проложить ссылки между "внешней" и "внутренней" моделью. Особенно если на HostVM и GuestVM разные языки, платформы и технологии. Всё программирование к этому можно свести, и теорию инженерных рассчётов, пожалуй, тоже. Имхо, вовсе не проблема маппировать одинаковые вещи или каталогизировать их -- проблема маппировать несводимые друг к другу вещи. А если отказаться от маппирования несводимых вещей -- то какая польза от такой неполной модели? (кроме как для онтологических целей: "и такое бывает, сынок"). Простейшие примеры несводимых вещей: Числа с возможностью null и числа без возможности null (можно описать через мета-категорию "значение", но практической ценности нет: операции описываются разные, всё прочее тоже разное, модель лишь привносит дополнительную сложность), "Процесс" в разных операционных системах (обладают разными свойствами, одинаково их моделировать нельзя, запись в виде "разновидность абстрактного процесса" не даёт никакого толка). Данные в разных типах баз данных или алгоритмах. Функции в разных языках программирования (обладающие спецэффектами, например, из-за разной обработки ситуаций типа NaN, Inf, null, итп, а также несводимости аргументов или внутренними условиями типа if(arg1 == 5) return 6; //Fixes bug #264826 ). P.S.: А "теория категорий" -- наиболее бесполезная конструкция в мире. Да и вообще, главная проблема моделирования -- модели получаются слишком сложными для человека, умеющего эффективно манипулировать крайне ограниченным числом сущностей. Более того, все эти мэппинги строить руками, даже с помощью инструмента или специального языка, слишком сложно и долго (ну какая там скорость логического мышления у человека? проверять 1 логическое условие в секунду?). Поэтому моделирование по-прежнему игрушка. Моделирование и построение нужных проекций по запросу с помощью ИИ -- наша единственная надежда. P.P.S. Извиняюсь за плохое знание неиболее корректных терминов предметной области моделирования или некорректное употребление этих терминов.