> есть предусловия и постусловия
Чтоб с этим нормально работать, хорошие типы уже нужны ;-)
Хотя и если просто описать операционно, конечно, требований к типам гораздо меньше.

зависимые типы для индуктивных данных антимодульны

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

В архитектурных языках архитектуры предприятия (типа ArchiMate) есть два элемента: один "процесс" для императивного процесса из шагов, а другой "функция" для вот такой вот "практики". Это всё описано у меня в учебнике "Системное мышление" — https://yadi.sk/i/aaZBihiJhw6i8w

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

Вот смотрите, как различаются описания Idris и Julia в их сравнении: https://www.slant.co/versus/133/5275/~julia_vs_idris

У Idris как раз  "Pro
Domain driven design and type driven development

Because of full dependent types in Idris, the programmer can focus more on modelling the domain with types and waste less time fixing common bugs that the type checker will catch. Dependent types help apply type driven development and a lot of code auto generation, making the compiler and type checker an ally in developing working software instead of just getting in the way" — это ровно то, зачем я пришёл в чатик по зависимым типам. Ибо я считал (зря считал), что подобные вопросы в сообществе любителей Idris не оффтоп.

В Julia "Pro
Strong dynamic typing

Dynamic and high level, but does not isolate the user from properly thinking about types. Can do explicit type signatures which is great for teaching structured thinking" — ничего про лёгкость domain driven design мы не слышим. Хотя это по факту не так, ибо там очень хорошая работа с пакетами — ты добавляешь описания мира с разных сторон, не перекомпилируя каждый раз всё заново вместе с библиотеками.

Не переживайте - в этой группе не оффтоп, мы ж её специально для этого и завели. 😊

Может, тогда и в названии это отразить? Типы в языках программирования, моделирования, представления знаний и жизни. Онтологические языки почему-то называют формально "языки представления знаний".

> Dependent types help apply type driven development and a lot of code auto generation, making the compiler and type checker an ally in developing working software instead of just getting in the way

На текущем уровне развития технологии, вот это предложение - почти полностью wishful thinking и маркетинг, к сожалению.

@ailevenchuk вопрос по Вашей стороне вопроса: какой теор-минимум следует изучить среднестатистическому типовику, чтобы иметь возможность осмысленно обсуждать онтологический фронтир?