Comments 6
Некорректно даны сравнения с альтернативами. Дано что-то вроде: все остальные могут быть мокрыми, а у Lean зато есть зелёный цвет.
Сравнение систем логического вывода, в общем-то, эквивалентно сравнению языков программирования. Про языки вы наверное в курсе, что там часто встречаются холивары. А теперь точно таким же образом вносите вклад в создание очередного холивара, но про логический вывод.
Может стоит сказать честнее? Вам нравится конкретный инструмент под названием Lean, вот и всё.
А если уже обосновывать как-то рационально, то стоит начинать со сравнения выразительных средств рассматриваемых систем. Где можно выразить идею короче? И внезапно окажется, что какие-то идеи короче в одном средстве, но другие идеи короче в другом. То есть всё зависит от задачи. Тогда нужно чётко формализовать задачу. Но вы же претендуете на универсальность. Значит задача остаётся неформализованой. Ну а следом остаются недоказуемыми любые утверждения о "лучшести" той или иной системы.
И напоследок, самым лучшим выразительным средством чаще всего является графическое представление. Их есть у вас? Ни у одного средства этого нет. Хотя вроде бы в сфере моделирования бизнеса это уже давно стандарт. Почему же вы предлагаете сделать шаг назад?
Да какое обоснование, это ж чатгопота. Автор поди и в глаза никакого lean не видел.
Даже не знаю с чего бы начать ответ но начну по частям.
а) Мы используем и разрабатываем инструменты моделирования на базе Eclipse Sirius
б) Хорошо знакомы и применяем традиционные инструменты моделирования.
в) Для трансформации моделей традиционную связку AQL+QVTo
В одном из проектов применялась верификация подобных преобразований на Isabelle\HOL,
а в этой статье я пишу не столько про изменение традиционных инструментов сколько про другой подход к верификации именно преобразования моделей (на языке Lean)
Мы начинаем внутри своей организации с этим экспериментировать, поэтому общие мысли и рассуждения почему нам кажется это полезным - в этой статье ;)
Экспериментировать за счёт работодателя - это прекрасно. Но чуть дальше вы столкнётесь с новыми "вызовами" для экспериментов.
Собственно ваш посыл тривиален - хочу рулить. Да так, что бы компьютер сам проверял, как там обезьяны внизу мои хотелки реализовали. Для этого выбрали логический вывод, мол как зададим системе "должна быть двухфакторная аутентификация", так сразу всё станет прекрасно.
Теперь реальность. В общепринятом подходе точно так же задают требования, хоть по аутентификации, хоть по чему ещё. Далее приёмка ПО - проверяем, есть или нет аутентификация. На глаз. То есть без компьютеров.
В вашем варианте то же самое, но с добавками "странного". То есть что вы там назадаёте в своей программе, никому не интересно ровно до тех пор, пока не придётся в вашу программу вбивать факт "аутентификация есть". Вот тут все начнут вас проклинать (и наверно уже начали), потому что им вместо простого человеческого заполнения какого-нибудь вордовского шаблона придётся учить вами выбранный язык, который явно не для большинства корпоративных работников. И после изучения они вбивают всё тот же шаблон - вот тебе тупая машина куча слов на твоём безумном языке, которые переводятся всё так же - у нас есть аутентификация. То есть вместо простоты вы вводите ненужное переусложнение, заставляя людей переводить с человеческого на машинный.
Допустим вам важен контроль (за всем сразу, а как иначе?). Но и для этого давно придумали намного более простые средства. Создаёте простейшую БД со списком ваших хотелок. В таблице "хочу" будут поля "что хочу" и "сделано". И в поле "сделано" живые люди ставят галку. Всё. Просто и присутствует полный контроль. Вместо проверки - простейший запрос. А на сколько всё сложнее у вас?
Я до вас хочу донести простую мысль - издеваетесь вы над людьми, прикрываясь экспериментами. И вообще, опыты над людьми запрещены, а вы всё туда же.
Выберите простой вариант и люди вас полюбят. Особенно если вы уже испугали их сложным. Теперь банальный переход на обычный вариант работы сделает всех, кому вы там предписали Lean изучать, просто счастливыми. Ну и так, мелочь - оно и вам будет проще без Lean, потому что это избыточная и ничем не оправданная сложность.
Итогом вашего Lean будет всё та же программа, но на языке, не предназначенном для написания программ. Вам придётся делать всё, что делает программист ниже вас. И вы станете теми программистами, для которых сверху опять придумают писать "логический вывод", снова выдумывая средства для написания программ. Ну и в итоге ни у вас, ни у тех кто сверху, ничего не получится, потому что инструмент не предназначен для полноценного написания программ.
Хотя вполне возможно, сейчас вы просто не поняли, про что я говорю. Опыт приходит с набитыми шишками. Так что набивайте. Но лучше только свои, то есть не бейте всех тех, кто снизу. Они ни в чём не виноваты. Не смотря на весь ваш боевой задор.
Господи что за бред,
У вас какая то фантазийная история, которую вы сами придумали.
Применение у этого решения совершено другое, не имеющее ничего общего с тем что вы написали.
Вместо того чтобы конструктивно написать, я не понял, подскажите границы решаемой задачи или какое то другое уточнение, для каких проблем.
Вместо этого вы придумали сами какую то историю сами её раскритиковали, придумали какой то образ моих личных и профессиональных качеств и его раскритиковали.
Я думал что хабр чем то по качеству комментариев должен отличаться от пикабу.
Моделирование с верификацией междоменных теорем на языке Lean