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

Ну вот идея этого чата была (как видно из заголовка), как формальная типизация языков программирования меняется на менее формальную языков моделирования и ещё менее формальную (не как в good old AI на Прологе, а как в современных нейросетях, работающих с естественным языком). Но собрались тут люди, которые в сторону relax типизации вообще не смотрят, а движение у них ровно наоборот, в сторону закручивания гаек формализации. Понятна их история, понятны их интересы, понятно всё — но моделирование и представление знаний в этом направлении где-то с 2012 года больше не живёт. Мощное движение "онтологов-логиков" где-то померло в 2013 году, работ 2014 года значимых уже нет, полная зима и ледниковый период, остались только академические исследования за деньги налогоплательщиков.

Поэтому я повздыхал-повздыхал, и мы нашли другие решения, и они очень круто работают на практике. Текущий вариант вошёл в учебник "Системное мышление 2022", курс "Системный менеджмент 2021" и т.д..

Вот я опубликовал фрагмент текста про эту многоуровневую объективацию как многоуровневую работу с типами: https://ailev.livejournal.com/1594529.html

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

И инструментарий там специфический. Вот мы провели месяц назад семинар ШСМ по опыту использования coda.io (https://www.youtube.com/watch?v=0_WycjiSbJg). И вот заметки про этот инструментарий работы с типами в "серой зоне" с этого семинара:
-- coda.io это инструмент моделирования: мета-мета-модель это наша новация (поддерживается курсами ШСМ), метамодель делается с участием subject expert и по факту это один из изводов DDD, операционная модель делается "просто сотрудниками". Важно: владелец мета-мета-модели (методолог/онтолог/когнитолог) ведёт беседу с subject expert и заставляет отмоделировать его предмет более полно, чем отмоделировал бы сам специалист в своём предмете. Мета-мета-модель содержит в себе чеклист моделирования как такового (foundation ontology, upper ontology и в случае трудового кругозора даже часть middle ontology), это позволяет делать более качественные предметные мета-модели. Сама coda.io понимает важность мета-моделей, но там "стихийная шаблонизация" ad hoc, качество получаемых моделей проверяется subject expert не в момент проектирования, а только методом проб и ошибок.
-- получаемые "двухэтажные" связки мета-модель+модель по факту нужно рассматривать в рамках парадигмы DevOps (в смысле единства ведения разработки и эксплуатации) и digital twins (ибо в число моделей разработки, главными из которых являются архитектурные модели, включаются модели операционные, времени эксплуатации/operations).
-- изначально coda.io была нацелена на ведение блогов, то есть публикацию доков в открытый доступ. А потом всё переориентировалось, и сейчас мы имеем доки для интранета, а не интернета. Но ограничения остались. Мы же понимаем, что блоги могут существовать на двух уровнях: блоги модели и блоги метамодели. Блоги метамодели в coda.io -- это вполне себе "мышление моделированием", такой вот производственный zettelkasten. Что напрочь отсутствует и нужно как-то прикручивать болтами сбоку (или искать в каких-то опциях): управление конфигурацией моделей, возможность хотя бы откатиться на предыдущую версию метамодели после неудачных групповых правок командой шустрых мейкеров (wiki как раз выжило, ибо для ситуации коллективного редактирования гипертекста предоставлялись возможности откатки до предыдущих версий каждой страницы и возможность посмотреть, какие изменения и кем были сделаны в каждой следующей версии -- иначе не разобраться). Без решения вопроса об управлении конфигурацией разработка в coda.io опасна.

-- программирование на нормальных языках в coda.io делается просто: обработка ведётся во внешних по отношению к coda.io системах, которые цепляются через стандартные коннекторы. Coda.io тем самым используется главным образом для моделирования, а не обработки (low code как моделер, а code при потребности немедленно уходит в другие системы, где этим могут заняться специально обученные люди.
-- При этом не путаем: low code тут означает "возможности для продвинутого пользователя", но не "визуальный интерфейс с квадратиками и стрелочками". Визуальный интерфейс, признали, играет важную психологическую роль. Как когда-то говорил Eric Raymond хакерам: "на собеседование в крупные фирмы одевайтесь не как вы обычно, а как одеваются хакеры в Голливуде". Вот и тут: демонстрируйте вашу работу не в реляционном (таблицы, rich text) виде, как вы её делаете, а лубочными картинками из квадратиков и стрелочек, как это принято у насмотревшихся Голливудских фильмов об айтишниках менеджеров.
-- мы ни разу не лояльны coda.io, но это лучший по отношению цена/качество на сегодня моделер. Если убрать цену, то Иван Падабед считает на сегодня лучшим fibery.io, и вот полуторагодичной давности сравнение: https://fibery.io/blog/fibery-vs-coda-the-power-of-workarounds/. А цена? Вы не обойдётесь несколькими платными мейкерами на организацию, платить придётся за всех прикоснувшихся. Было бы интересно, если бы кто-то покопал сегодняшнее состояние.

А чат оказался про "строгая типизация в языках программирования, моделирования, представлениях знаний, и ещё более строгая, чем вы думаете".

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

Мы постоянно сталкиваемся с теми или иными случайными событиями. На самом деле, мы просто не можем охватить все детали, что ими движут. Сознание отбрасывает большое количество деталей, каким бы не был скрупулёзным наблюдатель. Подсознание работает немного иначе, но средств изучения, реверсинжиниринга мозга не существует)

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

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

С другой стороны я вижу PINN и прочий (любимый Вами же) SciML, в котором дифуры с физ. величинами, у которых опять же размерности...

> но средств изучения, реверсинжиниринга мозга не существует

MRI, fMRI? Не, не слышал... 😏

Ну, учитывая Ваше отношение и знание психологии — не удивительно.

> доказательства свойств нейронок опираются на формализм теории типов

А что есть почитать на эту тему?

Как обычно — статьи с конференций. 😊

Ну, справедливости ради, томография не настолько точна, чтобы на каждый нейрон посмотреть
Я бы не удивился, если в мозге есть нейроны-диктаторы, от активации которых зависят некоторые процессы

Так я эти статьи и попросил :)
Или хотя бы в какую сторону копать

> Я бы не удивился, если в мозге есть нейроны-диктаторы, от активации которых зависят некоторые процессы

Нет, мозг так не работает... 😂

MRI — да, не сильно точный, кроме того считывает НЕ непосредственную активность нейронов. Поэтому крысам и некоторым другим млекопитающим втыкают иглы прямо в мозг. Людям, на самом деле, тоже, но в редких особых случаях.

Почему вы так уверены, что он так не работает?

Так бы сразу @GabrielFallen и сказал, что он про формальную верификацию
А то напустил красивых слов про теорию типов

Когда-то немного знакомился с вопросом "как работает мозг". 😊

Интересная дихотомия... 😃

Люблю снисходительное отношение и отсутствие аргументов

Что видно по Вашему сообщению. Точнее, по двум крайним. 😉

Так почему Вы противопоставили формальную верификацию и терию типов? Какие Ваши аргументы? 😊

Я не противопоставлял, я из-за слов "опираются на формализм теории типов" подумал, что там ввели какую-то систему типов, определили операционную семантику, отображающую синтаксис в нейронные сети (???) и что-то на этой основе доказали

Видимо, ошибочно