В настоящее время я изучаю проверку модели (модальная логика, LTL, CTL, SAL model checker и т. Д.), И в свободное время я изучаю Idris, который является строго типизированным функциональным языком программирования, который поддерживает зависимые типы. Поскольку я рассматриваю как проверку модели, так и Идрис, я начинаю любопытно, как Идрис относится к формальным методам и проверке модели.Релевантность проверки модели в строго типизированных функциональных языках программирования?
Когда вы узнаете о проверке модели, кажется, что большинство примеров, поднятых, - это либо проверка систем, написанных императивным образом, либо аппаратных компонентов. Поэтому я озадачен релевантностью проверки модели на строго типизированных языках функционального программирования и, особенно, на зависимом типизированном языке, таком как Идрис, где мне кажется, что проверяющий тип уже делает фантастическую работу по проверке правильности. Моя интуиция, однако, говорит мне, что проверка модели может быть связана с частичными функциями, которые не дают никаких обещаний о прекращении.
Является ли проверка модели актуальной при использовании строгого и зависимого типизированного языка программирования, такого как Идрис?