На самом деле, начать лучше с Martin-Lof Type Theory. Это при условии, что интуиционистскую логику первого порядка и (Simply Typed) Lambda Calculus Вы уже знаете.

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

Её принято называть HoTT. 😉

@GabrielFallen Это, конечно, пример выдуманный. Домен: земельный налог с XIII века до сейчас и в будущее. Требуется поддерживать существующие операции и архив, но полностью избавиться от ручной работы с бумажками, кроме ingress старых данных (из архива или от плательщиков налога)

HTT это обычно Хоарова теория типов

Ну да. Пруверы, все дела — это бантики. А вот спросить "выдай мне все трактора красного цвета" — вот это да, самое оно. Вот пример IDE, которая работает с вычислениями над этим (там DSL на Питоне): https://github.com/TechInvestLab/dot15926/

Хорошая английская документация, примеры.

Вопрос: если бы мы делали такое сегодня и не были привязаны к EXPRESS или RDF или SQL, и хотели бы иметь "просто IDE языка программирования", что мы должны были бы взять?! Чтобы это было практично, а не просто высокотеоретично?!

@GabrielFallen HTDP никак не расскажет, как вообще подступаться к этой задаче, даже если 1) её прочитавший знает налоги вдоль и поперёк; 2) хорошо умеет писать программы.

зависит от того что вы хотите гарантировать в этой вашей земельной опердени

т.е. какая там логика запросов

Да какая разница? Чтобы ни хотели, в HTDP не сказано ничего про это. Дальше надо "чуйкой" делать.

так вы не программу разрабатываете

Та не, падажжи - вопрос же про "как вообще подступиться", про методику анализа/моделирования. Или даже методологию.

Если взять книгу по моделированию данных в базах данных, то там всё как раз хорошо: "моделируем так, либо так, вот trade-offs, а можем ещё так разложить. Декомпозируем в эту сторону или в эту, см. что за данные" А где такое для чего-нибудь более богатого, чем реляционная модель?

Если прочитавший знает налоги вдоль и поперёк, то он следуя HTDP начнёт их расписывать на эти самые atomic data - itemization - compound data.

@GabrielFallen А потом спохватится, что у него есть время, процессы, события, роли, вход/выход из ролей, и тому подобные весёлые штуки, про которые в HTDP ничего нет, потому что про моделирование мира там ничего нет.

Сколько раз банк присылал вам выписку, в которой итоговый баланс не соответствовал балансу последней транзакции (три банка у меня лично)? Сколько раз оказывалось, что какая-нибудь utility company не может переместить плательщика из одной квартиры в другую, потому что у них ломается алгоритм начисления какой-нибудь скидки? (один раз, хватило). Это ошибки моделирования от того, что нет никакой технологии моделирования, а есть ad hoc.

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

Easy! Время - atomic data, события - enumeration (или itemization, в зависимости от), роли - снова enumeration. Насчёт process не уверен, но в части How to Design Worlds по сути как раз про них - нужно будет освежить.

Только мне кажется, проблема у Вас в другом месте, но Вы пока ещё не осознали в каком именно...

Вот не про насос, а про задвижку модель данных.

Вот более полная форма.