Обсуждение

Однако Вы ищете оправданий, чтобы не писать на Java, хотя почти всё из тех идей, которые Вы пропагандируете, рассматривается в качестве новых расширений языка. Вывод: Вы не зарабатываете на жизнь программированием.

Из одного контекста JSON-LD в другой переводить может оказаться невозможно безо всяких попутных inference той или иной сложности. Интеллект может оказаться сосредоточен тут. Особенно, если заморочиться не формированием данных для той или иной целевой системы из своей, или импортом чужих данных себе, а описанием контекстов для родных представлений этих систем и попыткой сформировать словари, связывающие эти контексты, покрывающие knowledge gap между ними.

>> триплы это тупик. Начинать нужно сразу с n-арных предикатов >> Если нужно преобразовавать в триплы, то пусть солвер FOL это преобразует и оптимизирует где-то там внутри себя, а на поверхности должны быть паттерны, n-арные предикаты Думаю, на нижнем уровне этого стека всё равно останутся триплы (см., например https://serge-gorshkov.livejournal.com/42799.html?thread=262959#t262959 ). При этом я согласен, что инженерам моделировать реальный мир в тройках неудобно.

/// на нижнем уровне этого стека всё равно останутся триплы /// Как раз на нижнем уровне незачем зажимать движок и ограничивать себя в возможностях. Потому — ничем не ограниченный гиперграф.

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

Ну вот языки программирования, под которыми формальная модель, почему-то всегда маргинальны. А уж делать маргинальный язык, который имеет маргинальность в его свойствах -- так вообще пользователей будут полтора человека (автор языка и полинженера). Так что формальная модель пусть будет в хотелках пока, а там поглядим. Вот сахарность -- это выход на standalone. Но при развитии языка тут же окажется, что хочется иметь полнотьюринговость, полноFOLовость и т.д.. И уж лучше сразу eDSL делать -- ибо всё одно упрёмся в то, что на базе standalone DSL будем пытаться сделать GPL со всем там необходимым, да ещё и мультипарадигмальным. Нет, этой дорогой мы ходили уже, не нужно туда. Хотя justy_tylor вот пишет компилятор как раз для такого. Но он крутой, ему можно )))

/// тут же окажется, что хочется иметь полнотьюринговость /// А где-то есть неполнотьюринговые? Я не видел.

А в чем маргинальность к примеру Coq или HOL? Это серьезные инструменты, которыми применимы для промышленных проектов. Юзербейз у них достаточно большой. У Coq первый релиз был 30 лет назад. Просто это требует очень высокой квалификации, чтобы задействовать эти тулзы в промышленном проекте (не токо инженеров, а ваще). У меня есть подозрение что маргинальность немного в другом проявляется - в том смысле, что в некоторых странах просто исчезающе мало места для проектов, где их можно было бы применить. Но если с мировой точки зрения смотреть, то маргинальны как раз такие страны, которые не могут осваивать современные технологии (а они заопенсорщены, даже Микрософт свой Z3 заопенсорсило). Adam Chlipala полагает что в течении 10 лет формальные тулзы созреют настолько, что от них будет польза для гораздо более широкого набора проектов. https://media.ccc.de/v/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development Я лично с ним согласен, хотя может и чутка подольше :). Но не суть важно. Важно, что это уже real thing пусть пока еще дорогой и не всем доступный. Но я вот рассчитываю в следующем году применить для реального проекта формальные тулзятины. Лет десять пытался но не вышло, сейчас вот очередная итерация надеюсь будет.

Ежели немного упростить, то грубо говоря, в течении 10 лет за применение формальных методов начнут платить бабки на регулярной основе. Ну и общественность по этому поводу резко перестанет считать тех кто занимается формальными методами маргиналами. Как это было со статистиками, которые были типа маргинальны, но ща они типа кульные датасайентисты и все такое :). Хотя тут может не будет такого хайпа как с ML/DS, но не суть важно. Я лично вижу такое направление развитие и собираюсь в следующем году к нему присоединиться (в этом уже вряд ли получится :)). Как было сказано в немецкой рекламе Sun'а: Sie haben die Vision und wir die Tools. Wofuer warten wir? Проекты где треба формальные методы имеются, инструменты тоже. Пора уже применять, я считаю.

Хотя тут важно отметить, что вовсе необязательно использовать всякие Coq, HOL и проч подобные. Можно и попроще что-нить. Начинать конечно имеет смысл с чего-то попроще. Но аппетит приходит во время еды :).Так что все эти coq, hol, agda, idris, lean и проч никуда не денутся :)

https://stainless.epfl.ch/ вот кстати пример подхода о котором Вы пишете (верификационный eDSL на Скале) Но ИМХО это не менее маргинально нежели Coq :).

"Лет десять пытался но не вышло, сейчас вот очередная итерация надеюсь будет" -- ну вот я абсолютно с той же целью задаюсь тут вопросами, хотя меня не именно формальные методы интересуют (просто ответы идут от людей, которых формальные методы главным образом интересуют). Десять лет назад ответов не было, даже не было понятно, победят ли eDSL или standalone DSL, хотя про DSL было уже ясно, что они нужны. Но ответ опять, похоже, "через десять лет" ))) Хотя justy_tylor пишет свой GPL как хост для eDSL, а я за неимением альтернатив получше (хотя мне и указывают на тот же C#) подумываю о том, не задействовать ли eDSL на Julia. Ну, или расслабиться, заняться другими делами, а потом прийти ещё через десять лет и повторить вопросы )))

Тут видимо все очень зависит от роли/целей. Я "осторожно" предполагаю, что Вам оно в основном нужно, чтобы заявить клиентам/подопечным "используйте вот эту штуку, это типа круто и полезно". Посему должен быть достаточно высокий степень зрелости. Мне это нужно потому что я хочу использовать в реальных/промышленных проектаъ, и получить от этого пользу (получить более надежный софт, найти баги/проблемы, снизить затраты на достижение того или иного уровня качества). Лет 10 назад уже были проекты где это было ограниченно полезно (фин софт в моем случае), но все же затраты на это дело слишком велики (слишком сырые тулзы). Дорабатывать тулзы я не мог. Сейчас тулзы улучшились, и я нашел сферу, где формальные методы гораздо более актуальны (впрочем это все тот же финсофт :)). Посему для меня сейчас оптимальный момент этим заниматься (чтобы быть готовым к тому когда через 10 лет тут будет бурный рост). Ну и еще один аспект - в зависимости от целей, нам нужна разная степень крутости формальных методов. А значит и потребная выразительность ЯП разная. Для большинства применений хватит Скала, C# наверное тоже (не очень с ним знаком) ну и других языков на которых удобно делать eDSL (Haskell, Groovie, etc). Иногда даже крутой поддержки DSL не нужно. Я бы к примеру сейчас вместо Скалы начал с Котлин - это если в Жаба мире, ну и C# уверен не хуже. Потому что начинать лучше все равно с простых формальных методов, там где депендент типов особо не видно еще :). Но вот на перспективу их хочется иметь все равно :). Поэтому в отдаленной перспективе интересны подходы к метапрограммированию типа Lean Prover. Мне пока видятся такие направления (сугубо с моей колокольни): - онтологии как инструмент моделирования предметной области, с целей понимания требования, выявления противоречий и генерации базового кода из этих моделей - модели дизайн уровня, т.е. уточнение моделей предметной области, как они мапятся на всякие архитектуры/структуры и проч. В том числе протоколы. Выявление проблем (багов). - низкий уровень - генерация тестов, верификация программ Мне думается что суровые вещи типа депендент тайпс нужны преимущественно на нижнем уровне. Хотя всякие протоколы - это тоже круто, но там наверное можно без dependent types жить.

Всякие Charity, Epigram, Coq, Agda, Idris... Когда серьезно берутся в типах выражать логические утверждения, и делают там вычисления, эти вычисления обязаны гарантировано завершаться (см. также Total Functional Programming), в противном случае незавершающееся вычисление может служить доказательством чего угодно; а значит их язык не должен быть полным по Тьюрингу.