Где нужны "зависимые типы"?
Все хотят применять "depended types" в разработке больших сложный систем, но мало кто в этом добился хоть каких-нибудь заметных успехов.
Оно и понятно - "зависимые типы" очень усложняют жизнь, а разработкой таких систем занимаются опытные программисты, располагающие развитыми средствами отладки и тестирования. То есть привносимый геморрой не оправдывает потенциальные не слишком радикальные преимущества.
А вот во всяких DSL для конфигурирования, воркфлоу, всяких политик, "умных контрактов" в блокчейнах, скриптов для "интернета вещей", да и просто скриптов для автоматизации рутинной работы чего-то типа "зависимых типов" для обеспечения надежности остро не хватает.
Во первых все эти программы относительно простые, и даже усложнение их разработки в 3-4 раза не так уж и страшно, да и время компиляции от дополнительных проверок сильно не вырастет.
Во вторых средства разработки у них не развиты и врядли для столь узких ниш кто-то этим будет заморачиваться.
В третьих пишут их не профессиональные программисты, а специалисты в своих предметных областях.
Оно и понятно - "зависимые типы" очень усложняют жизнь, а разработкой таких систем занимаются опытные программисты, располагающие развитыми средствами отладки и тестирования. То есть привносимый геморрой не оправдывает потенциальные не слишком радикальные преимущества.
А вот во всяких DSL для конфигурирования, воркфлоу, всяких политик, "умных контрактов" в блокчейнах, скриптов для "интернета вещей", да и просто скриптов для автоматизации рутинной работы чего-то типа "зависимых типов" для обеспечения надежности остро не хватает.
Во первых все эти программы относительно простые, и даже усложнение их разработки в 3-4 раза не так уж и страшно, да и время компиляции от дополнительных проверок сильно не вырастет.
Во вторых средства разработки у них не развиты и врядли для столь узких ниш кто-то этим будет заморачиваться.
В третьих пишут их не профессиональные программисты, а специалисты в своих предметных областях.