Работы ведутся главным образом людьми по имени D. Spivak и P. Schultz с одной стороны (разные варианты Temporal Type Theory) и Stephan Merz с другой стороны (развитие и модификация TLA+ в сторону большего удобства). Вообще TLA+ это же просто комбинирование стандартной теории множеств с логикой TLA, чтобы получился язык спецификаций. Но TLA можно попробовать скомбинировать не с теорией множеств, а теорией типов (потому что ZFC во-первых нетипизирована, во-вторых overkill, в третьих доказывать там что-то компьютерно-проверябельно жесть как неудобно), той же HoTT. Stephan Merz некогда развил логику TLA, обобщение получилось удобным и аксиоматизируется поэлегантнее чем исходная TLA - называется TLA*. А потом он занимался проектами Isabelle/TLA* и Isabelle/TLA+ - реализацией этих штук поверх провера Isabelle. Чтобы практически удобно было применять, хочется помощи со стороны SAT/SMT-солверов и арифметических солверов, с этой целью он разработал полутипизированный вариант Isabelle/TLA+ и провёл ещё много всякой такой работы.
С третьей стороны есть Frank Pfenning, недавно сказавший новое слово в модальных логиках - Adjoint Logic, это скорее не про доказательства свойств отдельно от программ, пост-фактум, а про описание протоколов взаимодействия (session types) в мультиагентных системах так, что некоторые полезные свойства (liveness и deadlock-freedom) верны по построению, а другие доказываются на основе спецификации. Посмотрите его статьи “A Message-Passing Interpretation of Adjoint Logic”, “Domain-Aware Session Types”, “Resource-Aware Session Types for Digital Contracts”, “Manifest Deadlock-Freedom for Shared Session Types” и “A Shared-Memory Semantics for Mixed Linear and Non-Linear Session Types”.
С третьей стороны есть Frank Pfenning, недавно сказавший новое слово в модальных логиках - Adjoint Logic, это скорее не про доказательства свойств отдельно от программ, пост-фактум, а про описание протоколов взаимодействия (session types) в мультиагентных системах так, что некоторые полезные свойства (liveness и deadlock-freedom) верны по построению, а другие доказываются на основе спецификации. Посмотрите его статьи “A Message-Passing Interpretation of Adjoint Logic”, “Domain-Aware Session Types”, “Resource-Aware Session Types for Digital Contracts”, “Manifest Deadlock-Freedom for Shared Session Types” и “A Shared-Memory Semantics for Mixed Linear and Non-Linear Session Types”.
Reply
Leave a comment