?

Log in

No account? Create an account
светлое будущее
Mike Potanin potan
Previous Entry Share Flag Next Entry
Где нужны "зависимые типы"?
Все хотят применять "depended types" в разработке больших сложный систем, но мало кто в этом добился хоть каких-нибудь заметных успехов.
Оно и понятно - "зависимые типы" очень усложняют жизнь, а разработкой таких систем занимаются опытные программисты, располагающие развитыми средствами отладки и тестирования. То есть привносимый геморрой не оправдывает потенциальные не слишком радикальные преимущества.
А вот во всяких DSL для конфигурирования, воркфлоу, всяких политик, "умных контрактов" в блокчейнах, скриптов для "интернета вещей", да и просто скриптов для автоматизации рутинной работы чего-то типа "зависимых типов" для обеспечения надежности остро не хватает.
Во первых все эти программы относительно простые, и даже усложнение их разработки в 3-4 раза не так уж и страшно, да и время компиляции от дополнительных проверок сильно не вырастет.
Во вторых средства разработки у них не развиты и врядли для столь узких ниш кто-то этим будет заморачиваться.
В третьих пишут их не профессиональные программисты, а специалисты в своих предметных областях.
Tags:

DT не там хотят применять (и видимо преуспеют - в виде refined types это imho скоро будет мейнстримом) - а в разработке mission critical систем - которые как раз не большие и не слишком сложные - а вот издержки там не "3-4 раза" уже сейчас - а хорошо если 30-40 - со всеми процедурами контроля качества и сертификации.

Потому там любые средства дающие допгарантии и хотя бы частичную верификацию именно экономят силы и средства.

Ну там тоже можно - F*, как оказалось, умеет проносить условия. Т.е. вы пишете
условный цЫкл сообщений, а каждую вызываемую из него функцию верхнего уровня
делаете Tot хрень. (вызываемые же из них будут автопроверяться на Тот

module IsPositive

let is_positive i = i > 0

val is_double_positive : int -> Tot bool
let is_double_positive i = is_positive (i+i)

Хотя ему для практики не хватат перегрузки функций. :-( Ну и с плавучкой я
вообще не понимаю, что там происходит.

Edited at 2016-07-06 11:38 pm (UTC)

Это не там придумано точно (в ATS тоже так же) - F* интересен именно тем что на нем вполне удобно писать.

В действительности я думаю туда скоро еще начнут всовывать не только тотальность - но и ограничения по расходу ресурсов (стека, памяти, сложности) - что в именно mission critical надо.

(no subject) - rdia, 2016-07-07 02:39 pm (UTC)(Expand)
(no subject) - kouzdra, 2016-07-07 05:48 pm (UTC)(Expand)
(no subject) - rdia, 2016-07-07 06:53 pm (UTC)(Expand)
(no subject) - rdia, 2016-07-08 01:38 pm (UTC)(Expand)
(no subject) - rdia, 2016-07-07 02:42 pm (UTC)(Expand)
Это первое, что напрашивается. Но mission critical систем не так уж и много, особенно таких, что бы у разработчика и заказчика были ресурсы на формальную верификацию. Так что не думаю, что это будет сильно стимулировать развития данного направления.

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

На чем собственно SPARK например живет. Или такой вообще-то вовсе ужас как SCADE

В чистом виде не нужны. Потому что _способны_ дать профит только на стадии верификации кода, но _гарантируют_ огромный просёр ресурсов при его написании.

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

В общем нет уже - тот же F* совершенно юзабелен. Чем и интересен.

Цикл разработки всяких скриптов и конфигов очень короткий. При этом, часто отладка происходит в "боевой" среде, поскольку создание тестовой часто оказывается очень сложной. И один неудачный запуск может привести к потере данных или остановке сервиса (даже если не в продакшене, это может помешать работе других разработчиков).
По этому очень хочется, что бы верификация происходила как можно раньше, перед каждым применением.

Скрипты это exploratory. Как минимум REPL, а лучше Jupyter.

И самое выгодное в таких случаях - вложиться в автоматизацию создания песочниц.

(no subject) - potan, 2016-07-07 10:15 am (UTC)(Expand)
(no subject) - justy_tylor, 2016-07-07 10:31 am (UTC)(Expand)
Ну вот у thesz поднялся вопрос, что bash - это УЖАС-УЖАС-УЖАС. Но, реально, bash не так-то просто заменить чем-то. Нужны:

а) Ленивость.
б) Параллельность (хотя бы на уровне вызова программ).

Кроме того, если вводить строгую типизацию, то нужно сделать весёлый финт ушами с кавычками. А именно, они не должны быть обязательными:

ls "-la" "/home/potan"

аля всякие Haskell Shell заебёт кого угодно.

С третьей стороны, нужно, чтобы у любого введённого снаружи объекта обязательно сохранялось строковое описание, ведь иначе не будет работать ни grep, ни sed.

(no subject) - potan, 2016-07-07 03:01 pm (UTC)(Expand)
(no subject) - rdia, 2016-07-07 03:07 pm (UTC)(Expand)
(no subject) - potan, 2016-07-07 03:23 pm (UTC)(Expand)
(no subject) - rdia, 2016-07-08 01:48 pm (UTC)(Expand)
(no subject) - voidex, 2016-07-08 07:01 pm (UTC)(Expand)
(no subject) - rdia, 2016-07-08 07:45 pm (UTC)(Expand)
(no subject) - rdia, 2016-08-18 10:20 pm (UTC)(Expand)
(no subject) - potan, 2016-08-19 12:44 pm (UTC)(Expand)
(no subject) - rdia, 2016-08-19 01:30 pm (UTC)(Expand)
(no subject) - potan, 2016-08-19 02:07 pm (UTC)(Expand)
(no subject) - rdia, 2016-08-19 03:04 pm (UTC)(Expand)
(no subject) - rdia, 2016-08-19 06:29 pm (UTC)(Expand)
Так а куда в скриптах зависимые типы приткнуть? Это же замедлит скорость разработки в десятки раз. Может, кто-то и согласится тратить дни вместо минут для того, чтобы снизить вероятность факапа с 0.0001% до 0.00001%, но сомнительно, что таких задач много.

(no subject) - potan, 2016-07-27 01:27 pm (UTC)(Expand)
(no subject) - Valentin Budaev, 2016-07-28 01:37 am (UTC)(Expand)
Я зависимые типы вижу в районе проектирования всякого рода железа, не только компьютерного.

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

Там внутре систем для такого проектирования целый язык со своими связями и ограничениями, очень развесистиыми. Части плат сохраняют для повторного использования и так далее. И всё равно, разработка сложной платы это 4-9 месяцев, как повезёт.

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

Да возьми https://hackage.haskell.org/package/turtle или https://hackage.haskell.org/package/shelly или другие и добавь туда ЗТ. Попробуй.

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

(no subject) - potan, 2016-07-25 02:02 pm (UTC)(Expand)
(no subject) - thesz, 2016-07-25 04:32 pm (UTC)(Expand)
(no subject) - thesz, 2016-07-25 04:33 pm (UTC)(Expand)
(no subject) - potan, 2016-07-25 06:06 pm (UTC)(Expand)
(no subject) - potan, 2016-07-25 06:22 pm (UTC)(Expand)
Вопрос - там, в зависимых типах есть поддержки симметрии? Ну, что + симметричен, а - - антисимметричен?